src/HOL/Algebra/Group.thy
changeset 19931 fb32b43e7f80
parent 19783 82f365a14960
child 19981 c0f124a0d385
     1.1 --- a/src/HOL/Algebra/Group.thy	Tue Jun 20 14:51:59 2006 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Tue Jun 20 15:53:44 2006 +0200
     1.3 @@ -189,8 +189,7 @@
     1.4    assumes Units: "carrier G <= Units G"
     1.5  
     1.6  
     1.7 -lemma (in group) is_group: "group G"
     1.8 -  by (rule group.intro [OF prems]) 
     1.9 +lemma (in group) is_group: "group G" .
    1.10  
    1.11  theorem groupI:
    1.12    fixes G (structure)
    1.13 @@ -468,7 +467,7 @@
    1.14        and h: "h \<in> carrier H"
    1.15    shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
    1.16    apply (rule group.inv_equality [OF DirProd_group])
    1.17 -  apply (simp_all add: prems group_def group.l_inv)
    1.18 +  apply (simp_all add: prems group.l_inv)
    1.19    done
    1.20  
    1.21  text{*This alternative proof of the previous result demonstrates interpret.
    1.22 @@ -643,8 +642,7 @@
    1.23    assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
    1.24        x \<otimes> y = y \<otimes> x"
    1.25    shows "comm_group G"
    1.26 -  by (fast intro: comm_group.intro comm_monoid_axioms.intro
    1.27 -                  is_group prems)
    1.28 +  by intro_locales (simp_all add: m_comm)
    1.29  
    1.30  lemma comm_groupI:
    1.31    fixes G (structure)
    1.32 @@ -679,7 +677,7 @@
    1.33  
    1.34  lemma (in group) subgroup_imp_group:
    1.35    "subgroup H G ==> group (G(| carrier := H |))"
    1.36 -  using subgroup.subgroup_is_group [OF _ group.intro] .
    1.37 +  by (rule subgroup.subgroup_is_group)
    1.38  
    1.39  lemma (in group) is_monoid [intro, simp]:
    1.40    "monoid G"