isabelle: src/HOL/AxClasses/Product.thy@537206cc738f (annotated)

10134 537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	1	(* Title: HOL/AxClasses/Product.thy
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	2	ID: $Id$
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	3	Author: Markus Wenzel, TU Muenchen
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	4	*)
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	5
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	6	theory Product = Main:
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	7
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	8	axclass product < "term"
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	9
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	10	consts
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	11	product :: "'a::product => 'a => 'a" (infixl "[*]" 70)
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	12
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	13
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	14	instance bool :: product
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	15	by intro_classes
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	16
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	17	defs (overloaded)
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	18	product_bool_def: "x [*] y == x & y"
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	19
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	20	end

author	wenzelm
	Tue, 03 Oct 2000 18:30:56 +0200
changeset 10134	537206cc738f
child 10681	ec76e17f73c5
permissions	-rw-r--r--