isabelle: src/FOL/FOL.thy@051592f4236a (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"
8471 36446bf42b16 splitter setup; wenzelm parents: 7355 diff changeset	9	use "cladata.ML" setup Cla.setup setup clasetup
36446bf42b16 splitter setup; wenzelm parents: 7355 diff changeset	10	use "blastdata.ML" setup Blast.setup
7355 4c43090659ca proper bootstrap of IFOL/FOL theories and packages; wenzelm parents: 5887 diff changeset	11	use "FOL_lemmas2.ML"
8643 331f0c75e3dc added cong atts; wenzelm parents: 8471 diff changeset	12	use "simpdata.ML" setup simpsetup setup cong_attrib_setup
8471 36446bf42b16 splitter setup; wenzelm parents: 7355 diff changeset	13	setup "Simplifier.method_setup Splitter.split_modifiers"
36446bf42b16 splitter setup; wenzelm parents: 7355 diff changeset	14	setup Splitter.setup setup Clasimp.setup
4093 5e8f3d57dee7 added claset thy_data; wenzelm parents: 0 diff changeset	15
4854 d1850e0964f2 tuned setup; wenzelm parents: 4793 diff changeset	16	end

author	paulson
	Thu, 06 Jul 2000 13:28:36 +0200
changeset 9264	051592f4236a
parent 8643	331f0c75e3dc
child 9487	7e377f912629
permissions	-rw-r--r--