--- a/src/ZF/ex/Ring.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/ex/Ring.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Rings *}
-theory Ring = Group:
+theory Ring imports Group begin
(*First, we must simulate a record declaration:
record ring = monoid +