isabelle: src/ZF/AC/HH.thy@b50b8c0eec01 (annotated)

1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	1	(* Title: ZF/AC/HH.thy
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	2	ID: $Id$
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	3	Author: Krzysztof Grabczewski
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	4
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	5	The theory file for the proofs of
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	6	AC17 ==> AC1
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	7	AC1 ==> WO2
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	8	AC15 ==> WO6
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	9	*)
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	10
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: 1155 diff changeset	11	HH = AC_Equiv + Hartog + WO_AC + Let +
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	12
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	13	consts
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	14
1401 0c439768f45c removed quotes from consts and syntax sections clasohm parents: 1203 diff changeset	15	HH :: [i, i, i] => i
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	16
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	17	defs
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	18
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: 1155 diff changeset	19	HH_def "HH(f,x,a) == transrec(a, %b r. let z = x - (UN c:b. r`c)
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: 1155 diff changeset	20	in if(f`z:Pow(z)-{0}, f`z, {x}))"
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	21
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	22	end
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	23

author	paulson
	Fri, 03 Jan 1997 15:01:55 +0100
changeset 2469	b50b8c0eec01
parent 1478	2b8c2a7547ab
child 11317	7f9e4c389318
permissions	-rw-r--r--