[isabelle-dev] auto raises a TYPE exception
makarius at sketis.net
Tue May 28 15:02:19 CEST 2013
On Tue, 28 May 2013, Makarius wrote:
> The crash happens in Thm.bicompose_no_flatten (via Goal.retrofit, which
> is the basis of SELECT_GOAL).
This also touches the still open thread on SELECT_GOAL here
although that was about term variables, not type variables.
More information about the isabelle-dev