1.1 --- a/src/HOL/ex/MonoidGroup.thy	Thu Feb 01 20:43:41 2001 +0100
     1.2 +++ b/src/HOL/ex/MonoidGroup.thy	Thu Feb 01 20:43:59 2001 +0100
     1.3 @@ -11,23 +11,23 @@
     1.4  theory MonoidGroup = Main:
     1.5  
     1.6  record 'a monoid_sig =
     1.7 -  times :: "['a, 'a] => 'a"
     1.8 +  times :: "'a => 'a => 'a"
     1.9    one :: 'a
    1.10  
    1.11  record 'a group_sig = "'a monoid_sig" +
    1.12    inv :: "'a => 'a"
    1.13  
    1.14  constdefs
    1.15 -  monoid :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'b::more |) => bool"
    1.16 -  "monoid M == ALL x y z.
    1.17 -    times M (times M x y) z = times M x (times M y z) &
    1.18 -    times M (one M) x = x & times M x (one M) = x"
    1.19 +  monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b::more |) => bool"
    1.20 +  "monoid M == \<forall>x y z.
    1.21 +    times M (times M x y) z = times M x (times M y z) \<and>
    1.22 +    times M (one M) x = x \<and> times M x (one M) = x"
    1.23  
    1.24 -  group :: "(| times :: ['a, 'a] => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b::more |) => bool"
    1.25 -  "group G == monoid G & (ALL x. times G (inv G x) x = one G)"
    1.26 +  group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b::more |) => bool"
    1.27 +  "group G == monoid G \<and> (\<forall>x. times G (inv G x) x = one G)"
    1.28  
    1.29 -  reverse :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'b::more |) =>
    1.30 -    (| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'b |)"
    1.31 -  "reverse M == M (| times := %x y. times M y x |)"
    1.32 +  reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b::more |) =>
    1.33 +    (| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)"
    1.34 +  "reverse M == M (| times := \<lambda>x y. times M y x |)"
    1.35  
    1.36  end