*To*: Chris Capel <pdf23ds at gmail.com>*Subject*: Re: [isabelle] problem with opening proof*From*: Makarius <makarius at sketis.net>*Date*: Sat, 23 May 2009 11:43:15 +0200 (CEST)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <737b61f30905221631s604eeffbu37010699ec4b5369@mail.gmail.com>*References*: <737b61f30905212054n968f86di25c0c6e0bcb9308@mail.gmail.com> <4A1652EC.5050500@informatik.tu-muenchen.de> <737b61f30905221631s604eeffbu37010699ec4b5369@mail.gmail.com>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Fri, 22 May 2009, Chris Capel wrote:

"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?

I suppose if the mode is not proof(chain) then default is the same asrule? And otherwise it's the same as erule?

But why does it also fail for "proof (rule exI)"? What's the differencebetween rule and intro that allows the latter to succeed?

Makarius

**Follow-Ups**:**Re: [isabelle] problem with opening proof***From:*Dr. Brendan Patrick Mahony

**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] problem with opening proof
- Next by Date: Re: [isabelle] Problems with datatype definition
- 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