isabelle: src/HOL/AxClasses/Tutorial/Sigs.thy@a901bafe4578 (annotated)

1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	1	(* Title: HOL/AxClasses/Tutorial/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	Some polymorphic constants for the 'signature' parts of axclasses.
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	Sigs = HOL +
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	9
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	10	consts
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	11	"<*>" :: "['a, 'a] => 'a" (infixl 70)
2907 0e272e4c7cb2 inv -> inverse nipkow parents: 1247 diff changeset	12	inverse :: "'a => 'a"
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	13	"1" :: "'a" ("1")
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	14
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	15	end

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