# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1579283938 -3600
# Node ID a3f7f00b4fd8c4b862f11f0b60a103b7579f04a5
# Parent  5556ae257df9361da939930c1a1cbecfc2ec9292
Removed unnecessary and problematic trivial lemma from HOL-Algebra

diff -r 5556ae257df9 -r a3f7f00b4fd8 src/HOL/Algebra/Multiplicative_Group.thy
--- a/src/HOL/Algebra/Multiplicative_Group.thy	Thu Jan 16 17:04:42 2020 +0100
+++ b/src/HOL/Algebra/Multiplicative_Group.thy	Fri Jan 17 18:58:58 2020 +0100
@@ -646,11 +646,6 @@
   shows "x [^] d \<in> Units G"
     by (metis assms group.is_monoid monoid.nat_pow_closed units_group units_of_carrier units_of_pow)
 
-lemma (in comm_monoid) is_monoid:
-  shows "monoid G" by unfold_locales
-
-declare comm_monoid.is_monoid[intro?]
-
 lemma (in ring) r_right_minus_eq[simp]:
   assumes "a \<in> carrier R" "b \<in> carrier R"
   shows "a \<ominus> b = \<zero> \<longleftrightarrow> a = b"