isabelle: src/ZF/AC/HH.thy@0c439768f45c (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$
1203 a39bec971684 Ran expandshort and changed spelling of Grabczewski lcp parents: 1196 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	clasohm
	Sat, 09 Dec 1995 13:36:11 +0100
changeset 1401	0c439768f45c
parent 1203	a39bec971684
child 1478	2b8c2a7547ab
permissions	-rw-r--r--