isabelle: src/ZF/AC/AC18_AC19.thy@3d773439d844 (annotated)

1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	1	(* Title: ZF/AC/AC18_AC19.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: 1123 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	Additional definition used in the proof AC19 ==> AC1 which is a part
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	6	of the chain AC1 ==> AC18 ==> AC19 ==> AC1
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	7	*)
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	8
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	9	AC18_AC19 = AC_Equiv +
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	10
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	11	consts
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	12	u_ :: "i => i"
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	13
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	14	defs
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	15
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	16	u_def "u_(a) == {c Un {0}. c:a}"
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	17
1203 a39bec971684 Ran expandshort and changed spelling of Grabczewski lcp parents: 1123 diff changeset	18	end

author	clasohm
	Thu, 26 Oct 1995 12:49:02 +0100
changeset 1310	3d773439d844
parent 1203	a39bec971684
child 1401	0c439768f45c
permissions	-rw-r--r--