src/HOL/Algebra/Group.thy
changeset 19984 29bb4659f80a
parent 19981 c0f124a0d385
child 20318 0e0ea63fe768
     1.1 --- a/src/HOL/Algebra/Group.thy	Tue Jul 04 12:13:38 2006 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Tue Jul 04 14:47:01 2006 +0200
     1.3 @@ -658,7 +658,7 @@
     1.4    assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
     1.5        x \<otimes> y = y \<otimes> x"
     1.6    shows "comm_group G"
     1.7 -  by intro_locales (simp_all add: m_comm)
     1.8 +  by unfold_locales (simp_all add: m_comm)
     1.9  
    1.10  lemma comm_groupI:
    1.11    fixes G (structure)