isabelle: src/HOL/AxClasses/Tutorial/Product.thy@50ec59aff389 (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
8920 af5e09b6c208 new Isar version; wenzelm parents: 1247 diff changeset	6	theory Product = Main:;
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	7
18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	8	axclass
8920 af5e09b6c208 new Isar version; wenzelm parents: 1247 diff changeset	9	product < "term";
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	10	consts
8920 af5e09b6c208 new Isar version; wenzelm parents: 1247 diff changeset	11	product :: "'a::product => 'a => 'a" (infixl "[*]" 70);
1247 18b1441fb603 Various axiomatic type class demos; wenzelm parents: diff changeset	12
8920 af5e09b6c208 new Isar version; wenzelm parents: 1247 diff changeset	13	instance bool :: product;
af5e09b6c208 new Isar version; wenzelm parents: 1247 diff changeset	14	by intro_classes;
9363 86b48eafc70d defs (overloaded); wenzelm parents: 8920 diff changeset	15	defs (overloaded)
8920 af5e09b6c208 new Isar version; wenzelm parents: 1247 diff changeset	16	product_bool_def: "x [*] y == x & y";
af5e09b6c208 new Isar version; wenzelm parents: 1247 diff changeset	17
af5e09b6c208 new Isar version; wenzelm parents: 1247 diff changeset	18	end;

author	wenzelm
	Wed, 02 Aug 2000 19:40:14 +0200
changeset 9502	50ec59aff389
parent 9363	86b48eafc70d
child 10007	64bf7da1994a
permissions	-rw-r--r--