*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] thus, hence (was: Eliminating two quantifiers in structural proof)*From*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Fri, 19 Oct 2012 10:13:38 +0900*In-reply-to*: <alpine.LNX.2.00.1209242141570.24981@macbroy20.informatik.tu-muenchen.de>*References*: <CAHPz_MptGHQPi+5mtx+OeZSBuR=2yzib5mZMH1sZJuqV5NFZJw@mail.gmail.com> <CAAPnxw0bFKyUcf_puXQO+gPLHrsqVHFfqhyOTGxF=G5i22xHTQ@mail.gmail.com> <alpine.LNX.2.00.1209242141570.24981@macbroy20.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:16.0) Gecko/20121009 Thunderbird/16.0

Note that the abbreviations "thus == then show" and "hence == then have" are merely historical accidents. They require fewer bytes in memory, but more typing by the user and more explanations to newcomers. The reason is that the chaining or not chaining for elementary 'show' and 'have' elements are often changed during the proof development. And there are further combinators like 'also' and 'moreover' that can be combined with 'have' or 'show', and other goal elements like 'obtain' that can participate in the chaining of facts in the same manner. So there is a large combinatorial space of (then | from | with | ... | also | finally | moreover | ultimately) (have | show | obtain | interpret ...) which is better spelled out as such explicitly, without the somewhat pointless shortcuts 'hence' and 'thus' getting in the way.

cheers chris

**Follow-Ups**:**Re: [isabelle] thus, hence***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] download all the entries for all the packages needed
- Next by Date: Re: [isabelle] thus, hence
- Previous by Thread: Re: [isabelle] download all the entries for all the packages needed
- Next by Thread: Re: [isabelle] thus, hence
- Cl-isabelle-users October 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