isabelle: src/FOL/FOL.thy@38f96394c099 (annotated)

4093 5e8f3d57dee7 added claset thy_data; wenzelm parents: 0 diff changeset	1
7355 4c43090659ca proper bootstrap of IFOL/FOL theories and packages; wenzelm parents: 5887 diff changeset	2	theory FOL = IFOL
4c43090659ca proper bootstrap of IFOL/FOL theories and packages; wenzelm parents: 5887 diff changeset	3	files ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("FOL_lemmas2.ML"):
4093 5e8f3d57dee7 added claset thy_data; wenzelm parents: 0 diff changeset	4
7355 4c43090659ca proper bootstrap of IFOL/FOL theories and packages; wenzelm parents: 5887 diff changeset	5	axioms
4c43090659ca proper bootstrap of IFOL/FOL theories and packages; wenzelm parents: 5887 diff changeset	6	classical: "(~P ==> P) ==> P"
4093 5e8f3d57dee7 added claset thy_data; wenzelm parents: 0 diff changeset	7
7355 4c43090659ca proper bootstrap of IFOL/FOL theories and packages; wenzelm parents: 5887 diff changeset	8	use "FOL_lemmas1.ML"
4c43090659ca proper bootstrap of IFOL/FOL theories and packages; wenzelm parents: 5887 diff changeset	9	use "cladata.ML" setup Cla.setup setup clasetup
4c43090659ca proper bootstrap of IFOL/FOL theories and packages; wenzelm parents: 5887 diff changeset	10	use "blastdata.ML" setup Blast.setup
4c43090659ca proper bootstrap of IFOL/FOL theories and packages; wenzelm parents: 5887 diff changeset	11	use "FOL_lemmas2.ML"
4c43090659ca proper bootstrap of IFOL/FOL theories and packages; wenzelm parents: 5887 diff changeset	12	use "simpdata.ML" setup simpsetup setup Clasimp.setup
4093 5e8f3d57dee7 added claset thy_data; wenzelm parents: 0 diff changeset	13
4854 d1850e0964f2 tuned setup; wenzelm parents: 4793 diff changeset	14	end

author	paulson
	Fri, 18 Feb 2000 15:35:29 +0100
changeset 8255	38f96394c099
parent 7355	4c43090659ca
child 8471	36446bf42b16
permissions	-rw-r--r--