src/HOL/ex/MonoidGroup.thy
changeset 19736 d8d0f8f51d69
parent 17388 495c799df31d
child 21404 eb85850d3eb7
     1.1 --- a/src/HOL/ex/MonoidGroup.thy	Sat May 27 17:42:00 2006 +0200
     1.2 +++ b/src/HOL/ex/MonoidGroup.thy	Sat May 27 17:42:02 2006 +0200
     1.3 @@ -14,17 +14,17 @@
     1.4  record 'a group_sig = "'a monoid_sig" +
     1.5    inv :: "'a => 'a"
     1.6  
     1.7 -constdefs
     1.8 +definition
     1.9    monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => bool"
    1.10 -  "monoid M == \<forall>x y z.
    1.11 +  "monoid M = (\<forall>x y z.
    1.12      times M (times M x y) z = times M x (times M y z) \<and>
    1.13 -    times M (one M) x = x \<and> times M x (one M) = x"
    1.14 +    times M (one M) x = x \<and> times M x (one M) = x)"
    1.15  
    1.16    group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b |) => bool"
    1.17 -  "group G == monoid G \<and> (\<forall>x. times G (inv G x) x = one G)"
    1.18 +  "group G = (monoid G \<and> (\<forall>x. times G (inv G x) x = one G))"
    1.19  
    1.20    reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) =>
    1.21      (| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)"
    1.22 -  "reverse M == M (| times := \<lambda>x y. times M y x |)"
    1.23 +  "reverse M = M (| times := \<lambda>x y. times M y x |)"
    1.24  
    1.25  end