Re: [isabelle] About contradiction method
You will find it much easier if you read the examples in the Tutorial
rather than just trying out all the different methods. The
contradiction method is not used very often.
On 17 Jun 2008, at 21:30, Glauber Cabral wrote:
I've been writing proofs only with apply (method) because Isabelle
the main focus right now and I thought it should be enough at this
write proofs this way.
The problem is that I could not find any example or explanation
about how to
use contradiction method. When I use it, I got 2 goals: P x y and
not P x y,
and I couldn't find how to make Isabelle relates P with a function
already created. Can anyone tell me where do I found any explanation
example to understand how it works?
This archive was generated by a fusion of
Pipermail (Mailman edition) and