Re: [isabelle] missing theorems in development version





I've obtained what I gather is a copy of a recent development version of Isabelle, containing new/altered files
OrderedGroup.thy and Ring_and_Field.thy.

I now find that certain arithmetic theorems don't seem to exist anymore,
eg
 thm "add_minus_self" ;
*** Unknown theorem(s) "add_minus_self"
Exception- ERROR raised
> val add_minus_self_left = thm "add_minus_self_left" ;
*** Unknown theorem(s) "add_minus_self_left"
Exception- ERROR raised
> val add_minus_self_right = thm "add_minus_self_right" ;
*** Unknown theorem(s) "add_minus_self_right"
Exception- ERROR raised

"add_minus_self" is now called "add_diff_cancel".

The other two theorems are gone. When you use the simplifier you should not need them as they can now be proved automatically.

--
Steven Obua
Technische Universität München
Institut für Informatik
Boltzmannstr. 3
D-85748 Garching

Tel: ++49 (0)89 / 289-17328
EMail: obua at in.tum.de
Raum: 01.11.059






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