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

[Lars Noschinski]

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