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:
lemma
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.
Alex
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
