src/HOL/Algebra/Group.thy
 changeset 19931 fb32b43e7f80 parent 19783 82f365a14960 child 19981 c0f124a0d385
```--- a/src/HOL/Algebra/Group.thy	Tue Jun 20 14:51:59 2006 +0200
+++ b/src/HOL/Algebra/Group.thy	Tue Jun 20 15:53:44 2006 +0200
@@ -189,8 +189,7 @@
assumes Units: "carrier G <= Units G"

-lemma (in group) is_group: "group G"
-  by (rule group.intro [OF prems])
+lemma (in group) is_group: "group G" .

theorem groupI:
fixes G (structure)
@@ -468,7 +467,7 @@
and h: "h \<in> carrier H"
shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
apply (rule group.inv_equality [OF DirProd_group])
-  apply (simp_all add: prems group_def group.l_inv)
+  apply (simp_all add: prems group.l_inv)
done

text{*This alternative proof of the previous result demonstrates interpret.
@@ -643,8 +642,7 @@
assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
x \<otimes> y = y \<otimes> x"
shows "comm_group G"
-  by (fast intro: comm_group.intro comm_monoid_axioms.intro
-                  is_group prems)
+  by intro_locales (simp_all add: m_comm)

lemma comm_groupI:
fixes G (structure)
@@ -679,7 +677,7 @@

lemma (in group) subgroup_imp_group:
"subgroup H G ==> group (G(| carrier := H |))"
-  using subgroup.subgroup_is_group [OF _ group.intro] .
+  by (rule subgroup.subgroup_is_group)

lemma (in group) is_monoid [intro, simp]:
"monoid G"```