Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] missing theorems in development version

view this post on Zulip Email Gateway (Aug 17 2022 at 13:26):

From: Steven Obua <obua@in.tum.de>
"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.

view this post on Zulip Email Gateway (Aug 17 2022 at 13:26):

From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
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

Last updated: May 03 2024 at 04:19 UTC