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

1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	1	(* Title: ZF/AC/HH.thy
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	2	ID: $Id$
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	3	Author: Krzysztof Gr`abczewski
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
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	15	HH :: "[i, i, i] => i"
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	lcp
	Tue, 25 Jul 1995 17:31:53 +0200
changeset 1196	d43c1f7a53fe
parent 1155	928a16e02f9f
child 1203	a39bec971684
permissions	-rw-r--r--