[isabelle-dev] internal TYPE exception at lemma statement
krauss at in.tum.de
Mon Oct 4 11:33:09 CEST 2010
To avoid that this issue, encountered by Lars, gets lost, I'll re-raise
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