isabelle: src/HOL/AxClasses/Group/Sigs.thy@5423e06b9fe6 (annotated)

1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	1	(* Title: Sigs.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
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	6	Sigs = HOL +
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	7
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	8	axclass
2907 0e272e4c7cb2 inv -> inverse nipkow parents: 1247 diff changeset	9	inverse < term
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	10
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	11	axclass
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	12	one < term
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	13
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	14	consts
2907 0e272e4c7cb2 inv -> inverse nipkow parents: 1247 diff changeset	15	inverse :: 'a::inverse => 'a
0e272e4c7cb2 inv -> inverse nipkow parents: 1247 diff changeset	16	"1" :: 'a::one ("1")
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	17
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	18	end

author	wenzelm
	Thu, 16 Oct 1997 13:33:17 +0200
changeset 3884	5423e06b9fe6
parent 2907	0e272e4c7cb2
permissions	-rw-r--r--