| changeset 16417 | 9bc16273c2d4 |
| parent 15763 | b901a127ac73 |
| child 16637 | 62dff56b43d3 |
--- a/src/HOL/Algebra/CRing.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/Algebra/CRing.thy Fri Jun 17 16:12:49 2005 +0200 @@ -7,8 +7,8 @@ header {* Abelian Groups *} -theory CRing = FiniteProduct -files ("ringsimp.ML"): +theory CRing imports FiniteProduct +uses ("ringsimp.ML") begin record 'a ring = "'a monoid" + zero :: 'a ("\<zero>\<index>")