[isabelle] how do I rename a fact in isabelle?



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.  

Thank you in advance, 
   Andrei Popescu 








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