*To*: Brian Huffman <huffman at in.tum.de>, Christian Sternagel <c-sterna at jaist.ac.jp>*Subject*: Re: [isabelle] interpret/moreover/ultimately*From*: Makarius <makarius at sketis.net>*Date*: Wed, 14 Mar 2012 00:10:11 +0100 (CET)*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAAMXsia12ndAydyf5WKGDh8iWcO=u2eihQ0fxJy7nnL_xRGzOw@mail.gmail.com>*References*: <4F59FFE0.8010201@jaist.ac.jp> <CAAMXsia12ndAydyf5WKGDh8iWcO=u2eihQ0fxJy7nnL_xRGzOw@mail.gmail.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Fri, 9 Mar 2012, Brian Huffman wrote:

On Fri, Mar 9, 2012 at 2:04 PM, Christian Sternagel <c-sterna at jaist.ac.jp> wrote:Hi there, recently I experienced some strange behavior (Isabelle2011-1 in jedit) which is reproduced in the small example below: notepad begin fix l le B interpret preorder l le sorryAt this point in your proof script, try ML_val {* Thm.concl_of @{thm this} *} and you will see that there is a constant "prop :: prop => prop" wrapped around the conclusion of this fact, outside the "Trueprop". Then try ML_val {* Thm.concl_of @{thm `class.preorder l le`} *} And you will see that no "prop" constant is there.Perhaps Makarius can say more about what this "prop" constant is for,and why it appears in the theorem exported by the interpret command.

Makarius

**References**:**[isabelle] interpret/moreover/ultimately***From:*Christian Sternagel

**Re: [isabelle] interpret/moreover/ultimately***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Install Isabelle under Windows (with Cygwin)
- Next by Date: [isabelle] AFP in DBLP
- Previous by Thread: Re: [isabelle] interpret/moreover/ultimately
- Next by Thread: [isabelle] PxTP 2012 (IJCAR Workshop) - Call for Papers
- Cl-isabelle-users March 2012 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