src/HOL/Algebra/Module.thy

--- a/src/HOL/Algebra/Module.thy	Thu Aug 03 14:53:57 2006 +0200
+++ b/src/HOL/Algebra/Module.thy	Thu Aug 03 14:57:26 2006 +0200
@@ -4,9 +4,12 @@
     Copyright:  Clemens Ballarin
 *)
 
-header {* Modules over an Abelian Group *}
+theory Module imports Ring begin
+
 
-theory Module imports CRing begin
+section {* Modules over an Abelian Group *}
+
+subsection {* Definitions *}
 
 record ('a, 'b) module = "'b ring" +
   smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)