src/HOL/Algebra/Coset.thy

--- a/src/HOL/Algebra/Coset.thy	Thu Jun 21 17:28:50 2007 +0200
+++ b/src/HOL/Algebra/Coset.thy	Thu Jun 21 17:28:53 2007 +0200
@@ -138,10 +138,13 @@
   assumes hH: "h \<in> H"
   shows "H #> h = H"
   apply (unfold r_coset_def)
-  apply rule apply rule
-  apply clarsimp
-  apply (intro subgroup.m_closed)
-  apply assumption+
+  apply rule
+   apply rule
+   apply clarsimp
+   apply (intro subgroup.m_closed)
+     apply (rule is_subgroup)
+    apply assumption
+   apply (rule hH)
   apply rule
   apply simp
 proof -