src/HOL/ex/MonoidGroup.thy
changeset 11939 c5e69470f03b
parent 11019 e968e5bfe98d
child 14981 e73f8140af78
--- a/src/HOL/ex/MonoidGroup.thy	Thu Oct 25 22:42:50 2001 +0200
+++ b/src/HOL/ex/MonoidGroup.thy	Thu Oct 25 22:43:05 2001 +0200
@@ -18,15 +18,15 @@
   inv :: "'a => 'a"
 
 constdefs
-  monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b::more |) => bool"
+  monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => bool"
   "monoid M == \<forall>x y z.
     times M (times M x y) z = times M x (times M y z) \<and>
     times M (one M) x = x \<and> times M x (one M) = x"
 
-  group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b::more |) => bool"
+  group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b |) => bool"
   "group G == monoid G \<and> (\<forall>x. times G (inv G x) x = one G)"
 
-  reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b::more |) =>
+  reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) =>
     (| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)"
   "reverse M == M (| times := \<lambda>x y. times M y x |)"