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

1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	1	(* Title: HOL/AxClasses/Tutorial/ProductInsts.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	Instantiate the 'syntactic' class "product", then define "<*>" on type
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	6	"bool".
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	7
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	8	Note: This may look like Haskell-instance, but is not quite the same!
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	ProductInsts = Product +
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	bool :: product
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	15
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	16	defs
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	17	prod_bool_def "x <*> y == x & y::bool"
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	18
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	19	end

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