*To*: Andrei Popescu <uuomul at yahoo.com>*Subject*: Re: [isabelle] how do I rename a fact in isabelle?*From*: Makarius <makarius at sketis.net>*Date*: Sun, 8 Mar 2009 12:31:10 +0100 (CET)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <501891.93642.qm@web56102.mail.re3.yahoo.com>*References*: <501891.93642.qm@web56102.mail.re3.yahoo.com>

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

**Follow-Ups**:**Re: [isabelle] how do I rename a fact in isabelle?***From:*Andrei Popescu

**References**:**[isabelle] how do I rename a fact in isabelle?***From:*Andrei Popescu

- Previous by Date: [isabelle] how do I rename a fact in isabelle?
- Next by Date: Re: [isabelle] how do I rename a fact in isabelle?
- Previous by Thread: [isabelle] how do I rename a fact in isabelle?
- Next by Thread: Re: [isabelle] how do I rename a fact in isabelle?
- 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