src/HOL/Algebra/Group.thy
changeset 44472 6f2943e34d60
parent 41528 276078f01ada
child 44655 fe0365331566
     1.1 --- a/src/HOL/Algebra/Group.thy	Wed Aug 24 23:19:40 2011 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Wed Aug 24 23:20:05 2011 +0200
     1.3 @@ -154,7 +154,7 @@
     1.4      and G: "x \<in> Units G"  "y \<in> carrier G"  "z \<in> carrier G"
     1.5    then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z"
     1.6      by (simp add: m_assoc Units_closed del: Units_l_inv)
     1.7 -  with G show "y = z" by (simp add: Units_l_inv)
     1.8 +  with G show "y = z" by simp
     1.9  next
    1.10    assume eq: "y = z"
    1.11      and G: "x \<in> Units G"  "y \<in> carrier G"  "z \<in> carrier G"
    1.12 @@ -332,7 +332,7 @@
    1.13  proof -
    1.14    assume x: "x \<in> carrier G"
    1.15    then have "inv x \<otimes> (x \<otimes> inv x) = inv x \<otimes> \<one>"
    1.16 -    by (simp add: m_assoc [symmetric] l_inv)
    1.17 +    by (simp add: m_assoc [symmetric])
    1.18    with x show ?thesis by (simp del: r_one)
    1.19  qed
    1.20  
    1.21 @@ -372,7 +372,7 @@
    1.22  proof -
    1.23    assume G: "x \<in> carrier G"  "y \<in> carrier G"
    1.24    then have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"
    1.25 -    by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric])
    1.26 +    by (simp add: m_assoc) (simp add: m_assoc [symmetric])
    1.27    with G show ?thesis by (simp del: l_inv Units_l_inv)
    1.28  qed
    1.29  
    1.30 @@ -446,7 +446,7 @@
    1.31  lemma (in group) one_in_subset:
    1.32    "[| H \<subseteq> carrier G; H \<noteq> {}; \<forall>a \<in> H. inv a \<in> H; \<forall>a\<in>H. \<forall>b\<in>H. a \<otimes> b \<in> H |]
    1.33     ==> \<one> \<in> H"
    1.34 -by (force simp add: l_inv)
    1.35 +by force
    1.36  
    1.37  text {* A characterization of subgroups: closed, non-empty subset. *}
    1.38