Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Algebra/UnivPoly.thy
changeset 44821 a92f65e174cf
parent 44655 fe0365331566
child 44890 22f665a2e91c 
--- a/src/HOL/Algebra/UnivPoly.thy	Wed Sep 07 14:58:40 2011 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Wed Sep 07 09:02:58 2011 -0700
@@ -1818,7 +1818,7 @@
 
 lemma INTEG_cring: "cring INTEG"
   by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
-    zadd_zminus_inverse2 zadd_zmult_distrib)
+    left_minus left_distrib)
 
 lemma INTEG_id_eval:
   "UP_pre_univ_prop INTEG INTEG id"
isabelle