On 05.08.2010 09:24, Lars Noschinski wrote:
On 05.08.2010 07:33, John Matthews wrote:
lemma
"ALL (x::nat). x = y ==> False"
apply (erule allE)
After this step, the subgoal "?x = y ==> False" remains, which cannot be
proven. Else, we could prove:
schematic_lemma foo: "?x = y ==> False"
Forgot the type annotations here, should be "(?x::nat) = y ==> False"
-- lars
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
