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

1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	1	(* Title: HOL/AxClasses/Tutorial/Product.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	Define a 'syntactic' class "product" that is logically equivalent to
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	6	"term".
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	7	*)
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	8
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	9	Product = HOL +
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	product < term
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	13
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	14	consts
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	15	"<*>" :: "['a::product, 'a] => 'a" (infixl 70)
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	16
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	17	end

author	wenzelm
	Mon, 29 Nov 1999 15:52:49 +0100
changeset 8039	a901bafe4578
parent 1247	18b1441fb603
child 8920	af5e09b6c208
permissions	-rw-r--r--