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

author	wenzelm
	Mon, 18 Sep 2000 14:10:31 +0200
changeset 10015	8c16ec5ba62b
parent 10007	64bf7da1994a
permissions	-rw-r--r--