isabelle: src/HOL/ROOT.ML@82a5ca6290aa (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";
5219 924359415f09 functorized Clasimp module; wenzelm parents: 5183 diff changeset	24	use "$ISABELLE_HOME/src/Provers/clasimp.ML";
4296 aa84d9c62454 added Arith provers; wenzelm parents: 4222 diff changeset	25	use "$ISABELLE_HOME/src/Provers/Arith/nat_transitive.ML";
aa84d9c62454 added Arith provers; wenzelm parents: 4222 diff changeset	26	use "$ISABELLE_HOME/src/Provers/Arith/cancel_sums.ML";
aa84d9c62454 added Arith provers; wenzelm parents: 4222 diff changeset	27	use "$ISABELLE_HOME/src/Provers/Arith/cancel_factor.ML";
4320 24d9e6639cd4 Moved the quantifier elimination simp procs into Provers. nipkow parents: 4296 diff changeset	28	use "$ISABELLE_HOME/src/Provers/quantifier1.ML";
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	29
1338 d2fc3bfaee7f changed simpset of "HOL" clasohm parents: 1301 diff changeset	30	use_thy "HOL";
4088 9be9e39fd862 added thy_data; wenzelm parents: 4024 diff changeset	31	use "hologic.ML";
9be9e39fd862 added thy_data; wenzelm parents: 4024 diff changeset	32	use "cladata.ML";
9be9e39fd862 added thy_data; wenzelm parents: 4024 diff changeset	33	use "simpdata.ML";
9be9e39fd862 added thy_data; wenzelm parents: 4024 diff changeset	34
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	35	use_thy "Ord";
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	36	use_thy "subset";
4864 3abfe2093aa0 removed typedef.ML, record.ML; wenzelm parents: 4758 diff changeset	37	use "Tools/typedef_package.ML";
5105 0ff5bec04d02 tuned Inductive.thy; wenzelm parents: 5097 diff changeset	38	use_thy "Sum";
0ff5bec04d02 tuned Inductive.thy; wenzelm parents: 5097 diff changeset	39	use_thy "Gfp";
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	40
4864 3abfe2093aa0 removed typedef.ML, record.ML; wenzelm parents: 4758 diff changeset	41	use "Tools/record_package.ML";
3abfe2093aa0 removed typedef.ML, record.ML; wenzelm parents: 4758 diff changeset	42	use_thy "Record";
4573 fe504f608835 added record.ML; wenzelm parents: 4517 diff changeset	43
5183 89f162de39cf Adapted to new datatype package. berghofe parents: 5124 diff changeset	44	use_thy "NatDef";
4296 aa84d9c62454 added Arith provers; wenzelm parents: 4222 diff changeset	45
5097 6c4a7ad6ebc7 Adapted to new inductive definition package. berghofe parents: 5078 diff changeset	46	use "Tools/inductive_package.ML";
5105 0ff5bec04d02 tuned Inductive.thy; wenzelm parents: 5097 diff changeset	47	use_thy "Inductive";
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	48
5183 89f162de39cf Adapted to new datatype package. berghofe parents: 5124 diff changeset	49	use "Tools/datatype_aux.ML";
89f162de39cf Adapted to new datatype package. berghofe parents: 5124 diff changeset	50	use "Tools/datatype_prop.ML";
89f162de39cf Adapted to new datatype package. berghofe parents: 5124 diff changeset	51	use "Tools/datatype_rep_proofs.ML";
89f162de39cf Adapted to new datatype package. berghofe parents: 5124 diff changeset	52	use "Tools/datatype_abs_proofs.ML";
89f162de39cf Adapted to new datatype package. berghofe parents: 5124 diff changeset	53	use "Tools/datatype_package.ML";
89f162de39cf Adapted to new datatype package. berghofe parents: 5124 diff changeset	54	use "Tools/primrec_package.ML";
89f162de39cf Adapted to new datatype package. berghofe parents: 5124 diff changeset	55
89f162de39cf Adapted to new datatype package. berghofe parents: 5124 diff changeset	56	use_thy "Arith";
89f162de39cf Adapted to new datatype package. berghofe parents: 5124 diff changeset	57	use "arith_data.ML";
89f162de39cf Adapted to new datatype package. berghofe parents: 5124 diff changeset	58
1515 4ed79ebab64d Introduced normalize_thm into HOL.ML nipkow parents: 1496 diff changeset	59	use_thy "RelPow";
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	60	use_thy "Finite";
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	61	use_thy "Sexp";
5124 1ce3cccfacdb stepping stones: Recdef, Main; wenzelm parents: 5110 diff changeset	62	use_thy "Recdef";
3981 b4f93a8da835 Added the new theory Map. nipkow parents: 3947 diff changeset	63	use_thy "Map";
4896 4727272f3db6 New syntax for function update; moved to main HOL directory paulson parents: 4864 diff changeset	64	use_thy "Update";
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	65
5107 2edf5dfb02f3 Replaced "use_dir" command by "use", because nested calls berghofe parents: 5105 diff changeset	66	cd "Integ";
5110 2497807020fa fixed Integ; wenzelm parents: 5107 diff changeset	67	use_thy "Bin";
5107 2edf5dfb02f3 Replaced "use_dir" command by "use", because nested calls berghofe parents: 5105 diff changeset	68	cd "..";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: 4896 diff changeset	69
3195 dcb458d38724 Preliminary TFL versions paulson parents: 2857 diff changeset	70	(TFL: recursive function definitions)
4517 fad9b7479dbe tuned; wenzelm parents: 4320 diff changeset	71	cd "$ISABELLE_HOME/src/TFL";
3195 dcb458d38724 Preliminary TFL versions paulson parents: 2857 diff changeset	72	use "sys.sml";
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: 4896 diff changeset	73	cd "$ISABELLE_HOME/src/HOL";
3195 dcb458d38724 Preliminary TFL versions paulson parents: 2857 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
1165 97b2bb5d43c3 renamed CHOL to HOL clasohm parents: 1024 diff changeset	80	val HOL_build_completed = (); (indicate successful build)

author	paulson
	Wed, 05 Aug 1998 10:57:25 +0200
changeset 5253	82a5ca6290aa
parent 5219	924359415f09
child 5298	81716d9b2b09
permissions	-rw-r--r--