src/HOL/Algebra/Group.thy
changeset 14551 2cb6ff394bfb
parent 14286 0ae66ffb9784
child 14651 02b8f3bcf7fe
     1.1 --- a/src/HOL/Algebra/Group.thy	Tue Apr 13 07:48:32 2004 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Tue Apr 13 09:42:40 2004 +0200
     1.3 @@ -410,6 +410,7 @@
     1.4    shows "semigroup (G(| carrier := H |))"
     1.5    using prems by fast
     1.6  
     1.7 +
     1.8  locale subgroup = submagma H G +
     1.9    assumes one_closed [intro, simp]: "\<one> \<in> H"
    1.10      and m_inv_closed [intro, simp]: "x \<in> H ==> inv x \<in> H"