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/CRing.thy
changeset 14286 0ae66ffb9784
parent 14213 7bf882b0a51e
child 14399 dc677b35e54f 
--- a/src/HOL/Algebra/CRing.thy	Wed Dec 10 14:27:50 2003 +0100
+++ b/src/HOL/Algebra/CRing.thy	Wed Dec 10 14:29:05 2003 +0100
@@ -90,7 +90,7 @@
   by (unfold comm_semigroup_def semigroup_def)
     (fast intro: comm_monoid.axioms a_comm_monoid)
 
-lemmas monoid_record_simps = semigroup.simps monoid.simps
+lemmas monoid_record_simps = partial_object.simps semigroup.simps monoid.simps
 
 lemma (in abelian_monoid) a_closed [intro, simp]:
   "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> y \<in> carrier G"
isabelle