Re: [isabelle] how do I rename a fact in isabelle?
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and