isabelle: src/HOL/ROOT.ML@858da18069d7 (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
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	15	(* Add user sections *)
4222 d7573d6d0513 refer to $ISABELLE_HOME/src; wenzelm parents: 4088 diff changeset	16	use "$ISABELLE_HOME/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
4222 d7573d6d0513 refer to $ISABELLE_HOME/src; wenzelm parents: 4088 diff changeset	19	use "$ISABELLE_HOME/src/Provers/simplifier.ML";
d7573d6d0513 refer to $ISABELLE_HOME/src; wenzelm parents: 4088 diff changeset	20	use "$ISABELLE_HOME/src/Provers/splitter.ML";
d7573d6d0513 refer to $ISABELLE_HOME/src; wenzelm parents: 4088 diff changeset	21	use "$ISABELLE_HOME/src/Provers/hypsubst.ML";
d7573d6d0513 refer to $ISABELLE_HOME/src; wenzelm parents: 4088 diff changeset	22	use "$ISABELLE_HOME/src/Provers/classical.ML";
d7573d6d0513 refer to $ISABELLE_HOME/src; wenzelm parents: 4088 diff changeset	23	use "$ISABELLE_HOME/src/Provers/blast.ML";
4296 aa84d9c62454 added Arith provers; wenzelm parents: 4222 diff changeset	24	use "$ISABELLE_HOME/src/Provers/Arith/nat_transitive.ML";
aa84d9c62454 added Arith provers; wenzelm parents: 4222 diff changeset	25	use "$ISABELLE_HOME/src/Provers/Arith/cancel_sums.ML";
aa84d9c62454 added Arith provers; wenzelm parents: 4222 diff changeset	26	use "$ISABELLE_HOME/src/Provers/Arith/cancel_factor.ML";
4320 24d9e6639cd4 Moved the quantifier elimination simp procs into Provers. nipkow parents: 4296 diff changeset	27	use "$ISABELLE_HOME/src/Provers/quantifier1.ML";
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	28
1338 d2fc3bfaee7f changed simpset of "HOL" clasohm parents: 1301 diff changeset	29	use_thy "HOL";
4088 9be9e39fd862 added thy_data; wenzelm parents: 4024 diff changeset	30	use "hologic.ML";
9be9e39fd862 added thy_data; wenzelm parents: 4024 diff changeset	31	use "cladata.ML";
9be9e39fd862 added thy_data; wenzelm parents: 4024 diff changeset	32	use "simpdata.ML";
9be9e39fd862 added thy_data; wenzelm parents: 4024 diff changeset	33
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	34	use_thy "Ord";
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	35	use_thy "subset";
4864 3abfe2093aa0 removed typedef.ML, record.ML; wenzelm parents: 4758 diff changeset	36	use "Tools/typedef_package.ML";
5105 0ff5bec04d02 tuned Inductive.thy; wenzelm parents: 5097 diff changeset	37	use_thy "Sum";
0ff5bec04d02 tuned Inductive.thy; wenzelm parents: 5097 diff changeset	38	use_thy "Gfp";
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	39
4864 3abfe2093aa0 removed typedef.ML, record.ML; wenzelm parents: 4758 diff changeset	40	use "Tools/record_package.ML";
3abfe2093aa0 removed typedef.ML, record.ML; wenzelm parents: 4758 diff changeset	41	use_thy "Record";
4573 fe504f608835 added record.ML; wenzelm parents: 4517 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";
89f162de39cf Adapted to new datatype package. berghofe parents: 5124 diff changeset	54
89f162de39cf Adapted to new datatype package. berghofe parents: 5124 diff changeset	55	use_thy "Arith";
89f162de39cf Adapted to new datatype package. berghofe parents: 5124 diff changeset	56	use "arith_data.ML";
89f162de39cf Adapted to new datatype package. berghofe parents: 5124 diff changeset	57
1515 4ed79ebab64d Introduced normalize_thm into HOL.ML nipkow parents: 1496 diff changeset	58	use_thy "RelPow";
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	59	use_thy "Finite";
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	60	use_thy "Sexp";
5124 1ce3cccfacdb stepping stones: Recdef, Main; wenzelm parents: 5110 diff changeset	61	use_thy "Recdef";
3981 b4f93a8da835 Added the new theory Map. nipkow parents: 3947 diff changeset	62	use_thy "Map";
4896 4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: 4864 diff changeset	63	use_thy "Update";
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	64
5107 2edf5dfb02f3 Replaced "use_dir" command by "use", because nested calls berghofe parents: 5105 diff changeset	65	cd "Integ";
5110 2497807020fa fixed Integ; wenzelm parents: 5107 diff changeset	66	use_thy "Bin";
5107 2edf5dfb02f3 Replaced "use_dir" command by "use", because nested calls berghofe parents: 5105 diff changeset	67	cd "..";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: 4896 diff changeset	68
3195 dcb458d38724 Preliminary TFL versions paulson parents: 2857 diff changeset	69	(TFL: recursive function definitions)
4517 fad9b7479dbe tuned; wenzelm parents: 4320 diff changeset	70	cd "$ISABELLE_HOME/src/TFL";
3195 dcb458d38724 Preliminary TFL versions paulson parents: 2857 diff changeset	71	use "sys.sml";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: 4896 diff changeset	72	cd "$ISABELLE_HOME/src/HOL";
3195 dcb458d38724 Preliminary TFL versions paulson parents: 2857 diff changeset	73
5124 1ce3cccfacdb stepping stones: Recdef, Main; wenzelm parents: 5110 diff changeset	74	(the all-in-one theory)
1ce3cccfacdb stepping stones: Recdef, Main; wenzelm parents: 5110 diff changeset	75	use_thy "Main";
1ce3cccfacdb stepping stones: Recdef, Main; wenzelm parents: 5110 diff changeset	76
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	77	print_depth 8;
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	78
1165 97b2bb5d43c3 renamed CHOL to HOL clasohm parents: 1024 diff changeset	79	val HOL_build_completed = (); (indicate successful build)

author	paulson
	Tue, 28 Jul 1998 16:30:56 +0200
changeset 5204	858da18069d7
parent 5183	89f162de39cf
child 5219	924359415f09
permissions	-rw-r--r--