src/HOL/ex/MonoidGroup.thy
changeset 9297 bafe45732b10
parent 9279 fb4186e20148
child 10357 0d0cac129618
--- a/src/HOL/ex/MonoidGroup.thy	Thu Jul 13 11:41:06 2000 +0200
+++ b/src/HOL/ex/MonoidGroup.thy	Thu Jul 13 11:41:40 2000 +0200
@@ -1,33 +1,31 @@
 (*  Title:      HOL/ex/MonoidGroup.thy
     ID:         $Id$
     Author:     Markus Wenzel
-    Copyright   1996 TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Monoids and Groups as predicates over record schemes.
 *)
 
-MonoidGroup = HOL + Record +
-
+theory MonoidGroup = Main:
 
 record 'a monoid_sig =
   times :: "['a, 'a] => 'a"
   one :: 'a
 
-record 'a group_sig = 'a monoid_sig +
+record 'a group_sig = "'a monoid_sig" +
   inv :: "'a => 'a"
 
 constdefs
-  monoid :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more::more |) => bool"
+  monoid :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'b::more |) => bool"
   "monoid M == ALL x y z.
     times M (times M x y) z = times M x (times M y z) &
     times M (one M) x = x & times M x (one M) = x"
 
-  group :: "(| times :: ['a, 'a] => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'more::more |) => bool"
+  group :: "(| times :: ['a, 'a] => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b::more |) => bool"
   "group G == monoid G & (ALL x. times G (inv G x) x = one G)"
 
-  reverse :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more::more |) =>
-    (| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |)"
+  reverse :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'b::more |) =>
+    (| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'b |)"
   "reverse M == M (| times := %x y. times M y x |)"
 
-
 end