--- a/src/HOL/ex/MonoidGroup.thy Thu Feb 01 20:43:41 2001 +0100
+++ b/src/HOL/ex/MonoidGroup.thy Thu Feb 01 20:43:59 2001 +0100
@@ -11,23 +11,23 @@
theory MonoidGroup = Main:
record 'a monoid_sig =
- times :: "['a, 'a] => 'a"
+ times :: "'a => 'a => 'a"
one :: 'a
record 'a group_sig = "'a monoid_sig" +
inv :: "'a => 'a"
constdefs
- 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"
+ monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b::more |) => 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 G == monoid G & (ALL x. times G (inv G x) x = one G)"
+ group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b::more |) => 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 |) =>
- (| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'b |)"
- "reverse M == M (| times := %x y. times M y x |)"
+ reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b::more |) =>
+ (| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)"
+ "reverse M == M (| times := \<lambda>x y. times M y x |)"
end