*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] proving a class instantiation.*From*: Makarius <makarius at sketis.net>*Date*: Fri, 12 Nov 2010 13:56:18 +0100 (CET)*In-reply-to*: <AANLkTin0s+J0oa+SUXO+R6fM8rcLdCkVwKosqSyapV7e@mail.gmail.com>*References*: <4CD93BE1.1080609@abo.fi> <AANLkTimoW5NDiPYez+RavGKXEHokjRHJMF35OwQfy5aV@mail.gmail.com> <alpine.LNX.1.10.1011091455540.16473@atbroy100.informatik.tu-muenchen.de> <AANLkTimMcLoOfSwK3SkdaJVcpAZ3bdGj-aeMemeTngyR@mail.gmail.com> <alpine.LNX.1.10.1011101640030.21694@atbroy100.informatik.tu-muenchen.de> <4CDAC3D3.8010607@in.tum.de> <alpine.LNX.1.10.1011101714540.23044@atbroy100.informatik.tu-muenchen.de> <AANLkTin0s+J0oa+SUXO+R6fM8rcLdCkVwKosqSyapV7e@mail.gmail.com>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Wed, 10 Nov 2010, Brian Huffman wrote:

On Wed, Nov 10, 2010 at 8:19 AM, Makarius <makarius at sketis.net> wrote:On Wed, 10 Nov 2010, Lars Noschinski wrote:My confusion stemmed from the fact that I like(d) to think of "!!x. A x ==> B x" as a convenient short-cut for the more verbose {fix x assume "A x" show "B x"}.It is in fact a short form of this: { fix x presume "A x" show "B x" ... }So of the two possible interpretations of show "!!x. A x ==> B x", youspecifically chose the version with 'presume' rather than 'assume'. Whydid you think this was the right choice? Comments on the mailing listhave clearly shown that users uniformly expect the 'assume'interpretation, and are thoroughly confused by the current behavior.

Abbreviating { fix assume "A x" show "B x" ... } as show "!!x. A x ==> B x" looses the advantages of Isar structure.

lemma foo by simp

lemma foo by simp

Makarius

**Follow-Ups**:**Re: [isabelle] proving a class instantiation.***From:*Tobias Nipkow

**References**:**[isabelle] proving a class instantiation.***From:*Viorel Preoteasa

**Re: [isabelle] proving a class instantiation.***From:*Brian Huffman

**Re: [isabelle] proving a class instantiation.***From:*Makarius

**Re: [isabelle] proving a class instantiation.***From:*Brian Huffman

**Re: [isabelle] proving a class instantiation.***From:*Makarius

**Re: [isabelle] proving a class instantiation.***From:*Makarius

**Re: [isabelle] proving a class instantiation.***From:*Brian Huffman

- Previous by Date: [isabelle] ismt update
- Next by Date: Re: [isabelle] proving a class instantiation.
- Previous by Thread: Re: [isabelle] proving a class instantiation.
- Next by Thread: Re: [isabelle] proving a class instantiation.
- Cl-isabelle-users November 2010 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