isabelle: src/ZF/AC/HH.thy@f98beaaa7c4f (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
11317 7f9e4c389318 X-symbols for set theory paulson parents: 1478 diff changeset	19	HH_def "HH(f,x,a) == transrec(a, %b r. let z = x - (\\<Union>c \\<in> b. r`c)
7f9e4c389318 X-symbols for set theory paulson parents: 1478 diff changeset	20	in if(f`z \\<in> 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	wenzelm
	Sat, 24 Nov 2001 16:54:32 +0100
changeset 12282	f98beaaa7c4f
parent 11317	7f9e4c389318
child 12776	249600a63ba9
permissions	-rw-r--r--