# [isabelle] elementary proofs

*To*: isabelle-users at cl.cam.ac.uk
*Subject*: [isabelle] elementary proofs
*From*: michel levy <michel.levy at imag.fr>
*Date*: Sat, 26 Mar 2016 23:48:52 +0100
*Mailscanner-null-check*: 1459637333.73314@CK8jsuPsL/j+pG/+aFlaBA
*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:38.0) Gecko/20100101 Thunderbird/38.6.0

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.*