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" sorry lemma "False" by (auto intro: foo[of 1 1, simplified]) -- lars _______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
