src/HOL/Algebra/Group.thy

--- a/src/HOL/Algebra/Group.thy	Tue Apr 13 07:48:32 2004 +0200
+++ b/src/HOL/Algebra/Group.thy	Tue Apr 13 09:42:40 2004 +0200
@@ -410,6 +410,7 @@
   shows "semigroup (G(| carrier := H |))"
   using prems by fast
 
+
 locale subgroup = submagma H G +
   assumes one_closed [intro, simp]: "\<one> \<in> H"
     and m_inv_closed [intro, simp]: "x \<in> H ==> inv x \<in> H"