[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

What's happening here, where have they gone?

Jeremy






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