*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Isar Proof*From*: TIMOTHY KREMANN <twksoa262 at verizon.net>*Date*: Tue, 17 Jun 2008 15:41:20 -0700 (PDT)

lemma "[| ALL x . (P (x::'a) => ~ Q x) /\ (P x => ~ R x) /\ (Q x => ~ R x); EX x . P x; EX x . Q x; EX x . R x|] ==> EX x y z. (~((x::'a) = y) /\ ~( x = z) /\ ~( y = z))" apply(elim ex_forward) apply(auto) done Can someone suggest an Isar equivalent for the above proof? Thanks, Tim

**Follow-Ups**:**Re: [isabelle] Isar Proof***From:*Dr. Brendan Patrick Mahony

**Re: [isabelle] Isar Proof***From:*Tobias Nipkow

- Previous by Date: [isabelle] About contradiction method
- Next by Date: [isabelle] Formal Methods in Use at Galois, an IJCAR Tutorial: Call for Participation
- Previous by Thread: Re: [isabelle] About contradiction method
- Next by Thread: Re: [isabelle] Isar Proof
- Cl-isabelle-users June 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list