*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] how do I rename a fact in isabelle?*From*: Andrei Popescu <uuomul at yahoo.com>*Date*: Sun, 8 Mar 2009 09:39:53 -0700 (PDT)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <Pine.LNX.4.64.0903081228080.13418@macbroy21.informatik.tu-muenchen.de>*Reply-to*: uuomul at yahoo.com

Thank you for your answer. The desire to change the name of a proposition in order to make that name available for an other proposition is, in my opinion, more than just a whim. Coming up with a suggestive fresh name is of course not a problem. But later in proofs, when I may need to invoke several facts related to several concepts, I would rather not lookup theorems in the database, but count on the fact that a theorem like foo_def applies what I as a designer (and not I as an implementor) choose to be the most natural "definition". (In particular, in Isabelle 2005, I used to set up the notations (and the simp database) in such a way that later I would not care to remember whether I have defined a non-recursive function with "fun" or with "constdefs".) Regards, Andrei --- On Sun, 3/8/09, Makarius <makarius at sketis.net> wrote: From: Makarius <makarius at sketis.net> Subject: Re: [isabelle] how do I rename a fact in isabelle? To: "Andrei Popescu" <uuomul at yahoo.com> Cc: isabelle-users at cl.cam.ac.uk Date: Sunday, March 8, 2009, 1:31 PM On Sat, 7 Mar 2009, Andrei Popescu wrote: > Say I define a function F with fun in a certain way, and then I prove > some facts which are nicer simplification rules, and would like to use > the name F.simps for these new facts. In Isabelle 2005, I used to > simply overwrite the name, but in Isabelle 2008 I am not allowed to do > this any longer. It seems that now I need to first rename the old facts > instead, but I do not know how. Well, you just need to come up with a fresh name, such as "F_simps". The original "F.simps" as produced by the function package will stay for eternity (due to strict monotonicity of the theory context). Once a logical entity is defined it cannot be changed. Makarius

**References**:**Re: [isabelle] how do I rename a fact in isabelle?***From:*Makarius

- Previous by Date: Re: [isabelle] how do I rename a fact in isabelle?
- Next by Date: Re: [isabelle] Isabelle's code generator for Haskell
- Previous by Thread: Re: [isabelle] how do I rename a fact in isabelle?
- Next by Thread: Re: [isabelle] Isabelle's code generator for Haskell
- Cl-isabelle-users March 2009 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