--- a/src/HOL/ex/MonoidGroup.thy Fri Jul 07 17:15:17 2000 +0200
+++ b/src/HOL/ex/MonoidGroup.thy Fri Jul 07 18:27:47 2000 +0200
@@ -17,15 +17,15 @@
inv :: "'a => 'a"
constdefs
- monoid :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |) => bool"
+ monoid :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more::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 & times M x (one M) = x"
+ times M (one M) x = x & times M x (one M) = x"
- group :: "(| times :: ['a, 'a] => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'more |) => bool"
+ group :: "(| times :: ['a, 'a] => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'more::more |) => bool"
"group G == monoid G & (ALL x. times G (inv G x) x = one G)"
- reverse :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |) =>
+ reverse :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more::more |) =>
(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |)"
"reverse M == M (| times := %x y. times M y x |)"