isabelle: src/HOL/AxClasses/Product.thy@6c7383f80ad1 (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	nipkow
	Sun, 09 Apr 2006 19:41:30 +0200
changeset 19390	6c7383f80ad1
parent 16417	9bc16273c2d4
permissions	-rw-r--r--