diff -r c530cb79ccbc -r 884dbbc8e1b3 src/HOL/Algebra/Ring.thy
--- 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