isabelle: src/HOL/AxClasses/Group/MonoidGroupInsts.thy@a901bafe4578 (annotated)

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 e853cd3f3ede tuned; 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

author	wenzelm
	Mon, 29 Nov 1999 15:52:49 +0100
changeset 8039	a901bafe4578
parent 7651	e853cd3f3ede
permissions	-rw-r--r--