summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/ex/MonoidGroup.thy

changeset 11939 | c5e69470f03b |

parent 11019 | e968e5bfe98d |

child 14981 | e73f8140af78 |

--- a/src/HOL/ex/MonoidGroup.thy Thu Oct 25 22:42:50 2001 +0200 +++ b/src/HOL/ex/MonoidGroup.thy Thu Oct 25 22:43:05 2001 +0200 @@ -18,15 +18,15 @@ inv :: "'a => 'a" constdefs - monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b::more |) => bool" + monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => 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 :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b |) => 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 |) => + reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => (| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)" "reverse M == M (| times := \<lambda>x y. times M y x |)"