| changeset 16417 | 9bc16273c2d4 |
| parent 15095 | 63f5f4c265dd |
| child 19783 | 82f365a14960 |
--- a/src/HOL/Algebra/Module.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/Algebra/Module.thy Fri Jun 17 16:12:49 2005 +0200 @@ -6,7 +6,7 @@ header {* Modules over an Abelian Group *} -theory Module = CRing: +theory Module imports CRing begin record ('a, 'b) module = "'b ring" + smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)