*To*: berghofe at mailbroy.informatik.tu-muenchen.de*Subject*: Re: [isabelle] more Isabelle2007 conversion pains*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Mon, 02 Jun 2008 10:48:57 +1000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <20080530185944.7l56wdapwgkos8oo@mailbroy.informatik.tu-muenchen.de>*References*: <6dbd4d000805081412v52d6d55dt298c8fa964204c8b@mail.gmail.com> <48240A4F.1070006@in.tum.de> <48278BA3.6090206@nicta.com.au> <48325DC2.9080904@rsise.anu.edu.au> <483A7E0B.60902@in.tum.de> <483B6872.7060902@rsise.anu.edu.au> <20080530185944.7l56wdapwgkos8oo@mailbroy.informatik.tu-muenchen.de>*User-agent*: Thunderbird 1.5.0.12 (X11/20070604)

berghofe at mailbroy.informatik.tu-muenchen.de wrote:

Quoting Jeremy Dawson <jeremy at rsise.anu.edu.au>:Stefan, thanks. But I now find a similar problem: the theorems x.mono, x.unfold and x.defs seem to have disappeared. Actually it seems the theorems x.mono, x.unfold already don't appear in Isabelle2005 for new-style theory files, but you could use an old-style theory file, or (sometimes) derive x.unfold from x.defs. But in Isabelle2007 you can't use an old-style theory file and even x.defs doesn't seem to exist. Where have all these theorems gone?Dear Jeremy,the problem with these rules is that they expose the internalrepresentationof inductive sets or predicates, which violates the principle ofinformationhiding. Since the internal representation has been changed recently,proofsusing these rules would not have worked any longer anyway, so Idecided toremove them. The 'official' way of proving something about an inductive definition is to use the introduction, induction and case analysis rules, and indeed all proofs using the x.unfold or x.defs rules can easily be rewritten to use these 'official' rules. Greetings, Stefan

Dear Stefan, Thanks for your reply.

Regards, Jeremy Dawson

**Follow-Ups**:**Re: [isabelle] more Isabelle2007 conversion pains***From:*Stefan Berghofer

- Next by Date: [isabelle] CFP - CATS 2009 -- Computing: The Australasian Theory Symposium
- Next by Thread: Re: [isabelle] more Isabelle2007 conversion pains
- Cl-isabelle-users June 2008 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