[isabelle] elementary proofs



I have tried (with success) a proof elementary
lemma facile1 : "P â (Q â P)"
  proof
    assume 1:"P"
    note 1
    show "Q â P"
    proof
      assume 2:"Q"
      from 1 show "P".
    qed
  qed

Then I have started another proof
lemma facile2 : "(P â Q) â (Q â R) â (P â R)"
  proof
    assume 1: "(P âQ)â (Q â R)"
    note 1
    show "P â R"
    proof
      assume 2:"P"
      note 2
      show "R"
      proof
But on the last line, on the word proof, I have the error "Failed to
apply initial proof method."
I don't see the difference between my both examples and why I have this
error.

Thank you in advance for an answer.

-- 
email : michel.levy at imag.fr
http://membres-liglab.imag.fr/michel.levy 




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