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.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.