isabelle: src/HOL/AxClasses/Product.thy@629f3a92863e (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
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 14981 diff changeset	6	theory Product imports Main begin
10134 537206cc738f moved axclass tutorial examples to top dir; wenzelm parents: diff changeset	7
12338 de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type"); wenzelm parents: 10681 diff changeset	8	axclass product < type
10134 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	immler@in.tum.de
	Thu, 26 Feb 2009 10:13:43 +0100
changeset 30151	629f3a92863e
parent 16417	9bc16273c2d4
permissions	-rw-r--r--