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

1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	1	(* Title: ZF/AC/AC18_AC19.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	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
1401 0c439768f45c removed quotes from consts and syntax sections clasohm parents: 1203 diff changeset	12	u_ :: i => i
1123 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	paulson
	Thu, 13 Jan 2000 17:31:30 +0100
changeset 8123	a71686059be0
parent 1478	2b8c2a7547ab
child 11317	7f9e4c389318
permissions	-rw-r--r--