[isabelle-dev] auto raises a TYPE exception

Tobias Nipkow nipkow at in.tum.de
Thu May 30 13:49:09 CEST 2013

Am 30/05/2013 13:41, schrieb Lawrence Paulson:
> The only question is whether Isabelle is important enough for such work to be seen as significant in a wider context.

Makarius is right, the interaction of schematic type variables and HOU has never
been nailed down properly and would be of interest to a larger community.


More information about the isabelle-dev mailing list