[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)"
show "Q â P"
from 1 show "P".
Then I have started another proof
lemma facile2 : "(P â Q) â (Q â R) â (P â R)"
assume 1: "(P âQ)â (Q â R)"
show "P â R"
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
Thank you in advance for an answer.
email : michel.levy at imag.fr
This archive was generated by a fusion of
Pipermail (Mailman edition) and