isabelle: src/HOL/AxClasses/Product.thy@28e42a90bea8 (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
10681 ec76e17f73c5 GPLed; wenzelm parents: 10134 diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
10134 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
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	7	theory Product = Main:
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	8
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	9	axclass product < "term"
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	10
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	11	consts
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	12	product :: "'a::product => 'a => 'a" (infixl "[*]" 70)
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
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	15	instance bool :: product
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	16	by intro_classes
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	17
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	18	defs (overloaded)
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	19	product_bool_def: "x [*] y == x & y"
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	20
537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	21	end

author	wenzelm
	Mon, 22 Oct 2001 18:02:50 +0200
changeset 11890	28e42a90bea8
parent 10681	ec76e17f73c5
child 12338	de0f4a63baa5
permissions	-rw-r--r--