src/HOL/AxClasses/Group/MonoidGroupInsts.thy
author wenzelm
Wed, 29 Sep 1999 14:40:15 +0200
changeset 7651 e853cd3f3ede
parent 1247 18b1441fb603
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1247
18b1441fb603 Various axiomatic type class demos;
wenzelm
parents:
diff changeset
     1
(*  Title:      MonoidGroupInsts.thy
18b1441fb603 Various axiomatic type class demos;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
18b1441fb603 Various axiomatic type class demos;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
18b1441fb603 Various axiomatic type class demos;
wenzelm
parents:
diff changeset
     4
18b1441fb603 Various axiomatic type class demos;
wenzelm
parents:
diff changeset
     5
Some class inclusions or 'abstract instantiations'.
18b1441fb603 Various axiomatic type class demos;
wenzelm
parents:
diff changeset
     6
*)
18b1441fb603 Various axiomatic type class demos;
wenzelm
parents:
diff changeset
     7
18b1441fb603 Various axiomatic type class demos;
wenzelm
parents:
diff changeset
     8
MonoidGroupInsts = Group + Monoid +
18b1441fb603 Various axiomatic type class demos;
wenzelm
parents:
diff changeset
     9
18b1441fb603 Various axiomatic type class demos;
wenzelm
parents:
diff changeset
    10
18b1441fb603 Various axiomatic type class demos;
wenzelm
parents:
diff changeset
    11
(* monoids are semigroups *)
18b1441fb603 Various axiomatic type class demos;
wenzelm
parents:
diff changeset
    12
18b1441fb603 Various axiomatic type class demos;
wenzelm
parents:
diff changeset
    13
instance
18b1441fb603 Various axiomatic type class demos;
wenzelm
parents:
diff changeset
    14
  monoid < semigroup            (Monoid.assoc)
18b1441fb603 Various axiomatic type class demos;
wenzelm
parents:
diff changeset
    15
18b1441fb603 Various axiomatic type class demos;
wenzelm
parents:
diff changeset
    16
18b1441fb603 Various axiomatic type class demos;
wenzelm
parents:
diff changeset
    17
(* groups are monoids *)
18b1441fb603 Various axiomatic type class demos;
wenzelm
parents:
diff changeset
    18
18b1441fb603 Various axiomatic type class demos;
wenzelm
parents:
diff changeset
    19
instance
7651
wenzelm
parents: 1247
diff changeset
    20
  group < monoid                ("Group.assoc", "Group.left_unit", "Group.right_unit")
1247
18b1441fb603 Various axiomatic type class demos;
wenzelm
parents:
diff changeset
    21
18b1441fb603 Various axiomatic type class demos;
wenzelm
parents:
diff changeset
    22
end