| changeset 75963 | 884dbbc8e1b3 |
| parent 70214 | 58191e01f0b1 |
| child 78522 | 918a9ed06898 |
--- a/src/HOL/Algebra/Ring.thy Wed Aug 24 06:21:06 2022 +0000 +++ b/src/HOL/Algebra/Ring.thy Wed Aug 24 08:22:13 2022 +0000 @@ -292,10 +292,8 @@ lemma is_monoid: "monoid R" by (auto intro!: monoidI m_assoc) -lemma is_ring: "ring R" - by (rule ring_axioms) +end -end thm monoid_record_simps lemmas ring_record_simps = monoid_record_simps ring.simps