*To*: Chris Capel <pdf23ds at gmail.com>*Subject*: Re: [isabelle] problem with opening proof*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Sat, 23 May 2009 08:01:06 +0200*Cc*: USR Isabelle <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <737b61f30905221631s604eeffbu37010699ec4b5369@mail.gmail.com>*Organization*: TU München, Lehrstuhl Software and Systems Engineering*References*: <737b61f30905212054n968f86di25c0c6e0bcb9308@mail.gmail.com> <4A1652EC.5050500@informatik.tu-muenchen.de> <737b61f30905221631s604eeffbu37010699ec4b5369@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.21 (X11/20090318)

Hi Chris, >>> fix ... >>> assume ... and ... >>> thus "EX x y. ..." >>> proof >> "proof" is short for "proof default", where the "default" method performs: > > In the Isar documentation it says "Unless given explicitly by the > user, the default initial method is “rule”". Is this inaccurate? Indeed, "default" is almost "rule", except if the proposition to prove involves class or locale predicates; this we can ignore here. > But why does it also fail for "proof (rule exI)"? What's the > difference between rule and intro that allows the latter to succeed? "rule" performs introduction if no facts are chained in, and elimination if some facts are chained in. "intro" only performs introduction. Hope this helps Florian -- Home: http://wwwbroy.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**References**:**[isabelle] problem with opening proof***From:*Chris Capel

**Re: [isabelle] problem with opening proof***From:*Florian Haftmann

**Re: [isabelle] problem with opening proof***From:*Chris Capel

- Previous by Date: Re: [isabelle] Problems with datatype definition
- Next by Date: Re: [isabelle] problem with opening proof
- Previous by Thread: Re: [isabelle] problem with opening proof
- Next by Thread: Re: [isabelle] problem with opening proof
- Cl-isabelle-users May 2009 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