author wenzelm Thu, 01 Feb 2001 20:43:59 +0100 changeset 11019 e968e5bfe98d parent 11018 71d624788ce2 child 11020 646c929b6293
tuned;
```--- 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```