--- a/src/HOL/Algebra/Coset.thy Fri Aug 01 17:41:37 2008 +0200
+++ b/src/HOL/Algebra/Coset.thy Fri Aug 01 18:10:52 2008 +0200
@@ -4,7 +4,7 @@
Stephan Hohe
*)
-theory Coset imports Group Exponent begin
+theory Coset imports Group begin
section {*Cosets and Quotient Groups*}