--- a/src/HOL/Algebra/Coset.thy Fri Oct 31 06:54:22 2003 +0100
+++ b/src/HOL/Algebra/Coset.thy Thu Nov 06 14:18:05 2003 +0100
@@ -46,7 +46,7 @@
*}
lemma (in group) is_coset:
"coset G"
- ..
+ by (rule coset.intro)
text{*Lemmas useful for Sylow's Theorem*}