[isabelle-dev] auto raises a TYPE exception

Makarius 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 mailing list