[isabelle-dev] [isabelle] safe for boolean equality

[Lars Noschinski]

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