Re: [isabelle] interpret/moreover/ultimately



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 sorry

At 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.

- Brian





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.