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)"