src/HOL/ex/MonoidGroup.thy
changeset 11939 c5e69470f03b
parent 11019 e968e5bfe98d
child 14981 e73f8140af78
     1.1 --- a/src/HOL/ex/MonoidGroup.thy	Thu Oct 25 22:42:50 2001 +0200
     1.2 +++ b/src/HOL/ex/MonoidGroup.thy	Thu Oct 25 22:43:05 2001 +0200
     1.3 @@ -18,15 +18,15 @@
     1.4    inv :: "'a => 'a"
     1.5  
     1.6  constdefs
     1.7 -  monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b::more |) => bool"
     1.8 +  monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => bool"
     1.9    "monoid M == \<forall>x y z.
    1.10      times M (times M x y) z = times M x (times M y z) \<and>
    1.11      times M (one M) x = x \<and> times M x (one M) = x"
    1.12  
    1.13 -  group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b::more |) => bool"
    1.14 +  group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b |) => bool"
    1.15    "group G == monoid G \<and> (\<forall>x. times G (inv G x) x = one G)"
    1.16  
    1.17 -  reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b::more |) =>
    1.18 +  reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) =>
    1.19      (| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)"
    1.20    "reverse M == M (| times := \<lambda>x y. times M y x |)"
    1.21