[isabelle-dev] internal TYPE exception at lemma statement

Alexander Krauss krauss at in.tum.de
Mon Oct 4 11:33:09 CEST 2010

Dear all,

To avoid that this issue, encountered by Lars, gets lost, I'll re-raise 
it here:

The following lemma statement raises an obscure internal TYPE exception:

   assumes "P foo" (is "P ?bar")
   shows "Q ?bar"

I assume that is-bindings cannot be used in the same structured 
statement. I also assume that this would be hard to support in general.

Is there any chance of getting a decent error message here, since it is 
actually quite natural to attempt something like this.


More information about the isabelle-dev mailing list