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.
Larry Paulson

On 17 Jun 2008, at 21:30, Glauber Cabral wrote:

I've been writing proofs only with apply (method) because Isabelle is not the main focus right now and I thought it should be enough at this moment to
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 I've already created. Can anyone tell me where do I found any explanation or
example to understand how it works?

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