isabelle: src/HOL/ROOT.ML@b3f6c39aaa2e (annotated)

1264 3eb91524b938 added local simpsets; removed IOA from 'make test' clasohm parents: 1165 diff changeset	1	(* Title: HOL/ROOT.ML
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	2	ID: $Id$
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	3	Author: Tobias Nipkow
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	4	Copyright 1993 University of Cambridge
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	5
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	6	Adds Classical Higher-order Logic to a database containing Pure Isabelle.
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	7	Should be executed in the subdirectory HOL.
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	8	*)
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	9
3947 eb707467f8c5 adapted to qualified names; wenzelm parents: 3578 diff changeset	10	val banner = "Higher-Order Logic";
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	11	writeln banner;
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	12
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	13	print_depth 1;
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	14
6392 e2ecfd8622ae tuned; wenzelm parents: 6349 diff changeset	15	(old-style theory syntax)
6260 a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	16	use "~~/src/Pure/section_utils.ML";
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	17	use "thy_syntax.ML";
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	18
6260 a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	19	use "~~/src/Provers/simplifier.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	20	use "~~/src/Provers/split_paired_all.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	21	use "~~/src/Provers/splitter.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	22	use "~~/src/Provers/hypsubst.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	23	use "~~/src/Provers/classical.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	24	use "~~/src/Provers/blast.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	25	use "~~/src/Provers/clasimp.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	26	use "~~/src/Provers/Arith/fast_lin_arith.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	27	use "~~/src/Provers/Arith/cancel_sums.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	28	use "~~/src/Provers/Arith/cancel_factor.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	29	use "~~/src/Provers/Arith/abel_cancel.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	30	use "~~/src/Provers/quantifier1.ML";
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	31
1338 d2fc3bfaee7f changed simpset of "HOL" clasohm parents: 1301 diff changeset	32	use_thy "HOL";
4088 9be9e39fd862 added thy_data; wenzelm parents: 4024 diff changeset	33	use "hologic.ML";
9be9e39fd862 added thy_data; wenzelm parents: 4024 diff changeset	34	use "cladata.ML";
9be9e39fd862 added thy_data; wenzelm parents: 4024 diff changeset	35	use "simpdata.ML";
9be9e39fd862 added thy_data; wenzelm parents: 4024 diff changeset	36
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	37	use_thy "Ord";
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	38	use_thy "subset";
4864 3abfe2093aa0 removed typedef.ML, record.ML; wenzelm parents: 4758 diff changeset	39	use "Tools/typedef_package.ML";
5105 0ff5bec04d02 tuned Inductive.thy; wenzelm parents: 5097 diff changeset	40	use_thy "Sum";
0ff5bec04d02 tuned Inductive.thy; wenzelm parents: 5097 diff changeset	41	use_thy "Gfp";
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	42
5183 89f162de39cf Adapted to new datatype package. berghofe parents: 5124 diff changeset	43	use_thy "NatDef";
4296 aa84d9c62454 added Arith provers; wenzelm parents: 4222 diff changeset	44
5097 6c4a7ad6ebc7 Adapted to new inductive definition package. berghofe parents: 5078 diff changeset	45	use "Tools/inductive_package.ML";
5105 0ff5bec04d02 tuned Inductive.thy; wenzelm parents: 5097 diff changeset	46	use_thy "Inductive";
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	47
5183 89f162de39cf Adapted to new datatype package. berghofe parents: 5124 diff changeset	48	use "Tools/datatype_aux.ML";
89f162de39cf Adapted to new datatype package. berghofe parents: 5124 diff changeset	49	use "Tools/datatype_prop.ML";
89f162de39cf Adapted to new datatype package. berghofe parents: 5124 diff changeset	50	use "Tools/datatype_rep_proofs.ML";
89f162de39cf Adapted to new datatype package. berghofe parents: 5124 diff changeset	51	use "Tools/datatype_abs_proofs.ML";
89f162de39cf Adapted to new datatype package. berghofe parents: 5124 diff changeset	52	use "Tools/datatype_package.ML";
89f162de39cf Adapted to new datatype package. berghofe parents: 5124 diff changeset	53	use "Tools/primrec_package.ML";
5560 c17471a9c99c tuned; wenzelm parents: 5501 diff changeset	54	use_thy "Datatype";
6907 870a953e0a8c added Numeral.thy; wenzelm parents: 6440 diff changeset	55	use_thy "Numeral";
5183 89f162de39cf Adapted to new datatype package. berghofe parents: 5124 diff changeset	56
5699 5b9a359e083c split_paired_all.ML; wenzelm parents: 5606 diff changeset	57	use "Tools/record_package.ML";
5b9a359e083c split_paired_all.ML; wenzelm parents: 5606 diff changeset	58	use_thy "Record";
5b9a359e083c split_paired_all.ML; wenzelm parents: 5606 diff changeset	59
6440 7c59a55bae94 added Tools/induct_method.ML; wenzelm parents: 6431 diff changeset	60	(TFL: recursive function definitions)
7c59a55bae94 added Tools/induct_method.ML; wenzelm parents: 6431 diff changeset	61	use_thy "WF_Rel";
7c59a55bae94 added Tools/induct_method.ML; wenzelm parents: 6431 diff changeset	62	cd "../TFL";
7c59a55bae94 added Tools/induct_method.ML; wenzelm parents: 6431 diff changeset	63	use "sys.sml";
7c59a55bae94 added Tools/induct_method.ML; wenzelm parents: 6431 diff changeset	64	cd "../HOL";
7c59a55bae94 added Tools/induct_method.ML; wenzelm parents: 6431 diff changeset	65	use "Tools/recdef_package.ML";
7c59a55bae94 added Tools/induct_method.ML; wenzelm parents: 6431 diff changeset	66	use "Tools/induct_method.ML";
5425 157c6663dedd Added function upto to List. nipkow parents: 5298 diff changeset	67	use_thy "Recdef";
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	68
5107 2edf5dfb02f3 Replaced "use_dir" command by "use", because nested calls berghofe parents: 5105 diff changeset	69	cd "Integ";
5501 a63e0c326e6c new files in Integ paulson parents: 5425 diff changeset	70	use_thy "IntDef";
5560 c17471a9c99c tuned; wenzelm parents: 5501 diff changeset	71	use "simproc.ML";
6914 ad689270a265 new theory IntDiv.thy paulson parents: 6907 diff changeset	72	use_thy "IntDiv";
5107 2edf5dfb02f3 Replaced "use_dir" command by "use", because nested calls berghofe parents: 5105 diff changeset	73	cd "..";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: 4896 diff changeset	74
5124 1ce3cccfacdb stepping stones: Recdef, Main; wenzelm parents: 5110 diff changeset	75	(the all-in-one theory)
1ce3cccfacdb stepping stones: Recdef, Main; wenzelm parents: 5110 diff changeset	76	use_thy "Main";
1ce3cccfacdb stepping stones: Recdef, Main; wenzelm parents: 5110 diff changeset	77
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	78	print_depth 8;
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	79
5501 a63e0c326e6c new files in Integ paulson parents: 5425 diff changeset	80	Goal "True"; (leave subgoal package empty)

author	wenzelm
	Fri, 09 Jul 1999 18:48:33 +0200
changeset 6953	b3f6c39aaa2e
parent 6914	ad689270a265
child 7032	d6efb3b8e669
permissions	-rw-r--r--