# HG changeset patch
# User wenzelm
# Date 981056639 -3600
# Node ID e968e5bfe98db776b66f3f1cb1ed0620d59acc63
# Parent  71d624788ce2723966801825d1120984d201e6e0
tuned;

diff -r 71d624788ce2 -r e968e5bfe98d src/HOL/ex/MonoidGroup.thy
--- 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