[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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and