*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] How do I write the sequent |- P in Isar using theorem*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Mon, 01 Jul 2013 22:15:04 -0500*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <alpine.LNX.2.00.1307012133040.25919@macbroy21.informatik.tu-muenchen.de>*References*: <51CE8C40.6020808@gmx.com> <alpine.LNX.2.00.1307012133040.25919@macbroy21.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 7/1/2013 2:44 PM, Makarius wrote:

The following versions lets you peek at the internal sequent (usingpostfix notation for the "antecedent" due to Larry); the slightlynested proof fragment ensures that the hypothetical facts actuallyshow up in the result:notepad begin note [[show_hyps]] ...After closing the block, the internal sequent is exported into theenclosing context, discharging the assumptions and turning them intovisible Pure rule structure using ==>.Likewise, the initial "theorem assumes A and B shows C" gives you theexported rule "A ==> B ==> C", not its sequent.As a user of Isabelle/Pure (and HOL as application within it), youshould never encounter the hypotheses of the internal sequents, onlythe exported versions with explicit rule structure.

Makarius,

The conjunction introduction rule becomes Gamma |- A Delta |- B ------------------------------- Gamma, Delta |- A & B The conclusion depends upon every assumption of A and of B.

I attached a screen shot and a PDF showing my notation experiments. Regards, GB

**Attachment:
130701_sequent_stuff.png**

**Attachment:
130701_sequent_stuff.pdf**

**Follow-Ups**:**Re: [isabelle] How do I write the sequent |- P in Isar using theorem***From:*Gottfried Barrow

**References**:

- Previous by Date: Re: [isabelle] How do I write the sequent |- P in Isar using theorem
- Next by Date: Re: [isabelle] How do I write the sequent |- P in Isar using theorem
- Previous by Thread: Re: [isabelle] How do I write the sequent |- P in Isar using theorem
- Next by Thread: Re: [isabelle] How do I write the sequent |- P in Isar using theorem
- Cl-isabelle-users July 2013 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