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

1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	1	(* Title: Group.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
2907 0e272e4c7cb2 inv -> inverse nipkow parents: 1247 diff changeset	6	Group = Sigs + Fun +
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	7
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	8	(* semigroups *)
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	9
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	10	axclass
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	11	semigroup < times
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	12	assoc "(x * y) * z = x * (y * z)"
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	13
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	14
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	15	(* groups *)
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	16
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	17	axclass
2907 0e272e4c7cb2 inv -> inverse nipkow parents: 1247 diff changeset	18	group < one, inverse, semigroup
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	19	left_unit "1 * x = x"
2907 0e272e4c7cb2 inv -> inverse nipkow parents: 1247 diff changeset	20	left_inverse "inverse x * x = 1"
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	21
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	22
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	23	(* abelian groups *)
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	24
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	25	axclass
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	26	agroup < group
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	27	commut "x * y = y * x"
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	28
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	29	end

author	wenzelm
	Fri, 18 Jul 1997 13:51:28 +0200
changeset 3531	f6cc9112f4e9
parent 2907	0e272e4c7cb2
permissions	-rw-r--r--