[isabelle] proof statement fails



Hi,

I have written

theory Let
imports Main
begin

  lemma "(2 :: nat) + 2 = 4"
    proof

Now, 'proof' results in

"empty result sequence -- proof command failed"

Otherwise, i.e. without Isar,

apply (auto)

finishes the proof, so the lemma itself is well-written. What else could fail?

- Gergely





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.