isabelle: src/HOL/ROOT.ML@4462ee172ef0 (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
7739 bfe45b716dfc tuned comment; wenzelm parents: 7703 diff changeset	6	Classical Higher-order Logic.
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	7	*)
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	8
3947 eb707467f8c5 adapted to qualified names; wenzelm parents: 3578 diff changeset	9	val banner = "Higher-Order Logic";
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	10	writeln banner;
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	11
7357 d0e16da40ea2 proper bootstrap of HOL theory and packages; wenzelm parents: 7237 diff changeset	12	use "hologic.ML";
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	13
6260 a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	14	use "~~/src/Provers/splitter.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	15	use "~~/src/Provers/hypsubst.ML";
19835 81d6dc597559 added updated version of IsaPlanner and substitution. dixon parents: 19174 diff changeset	16	use "~~/src/Provers/IsaPlanner/zipper.ML";
81d6dc597559 added updated version of IsaPlanner and substitution. dixon parents: 19174 diff changeset	17	use "~~/src/Provers/IsaPlanner/isand.ML";
81d6dc597559 added updated version of IsaPlanner and substitution. dixon parents: 19174 diff changeset	18	use "~~/src/Provers/IsaPlanner/rw_tools.ML";
81d6dc597559 added updated version of IsaPlanner and substitution. dixon parents: 19174 diff changeset	19	use "~~/src/Provers/IsaPlanner/rw_inst.ML";
18595 a52907967bae simplified EqSubst setup; wenzelm parents: 18529 diff changeset	20	use "~~/src/Provers/eqsubst.ML";
11685 c786d9ce558e use "~~/src/Provers/induct_method.ML"; wenzelm parents: 10766 diff changeset	21	use "~~/src/Provers/induct_method.ML";
6260 a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	22	use "~~/src/Provers/classical.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	23	use "~~/src/Provers/blast.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	24	use "~~/src/Provers/clasimp.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	25	use "~~/src/Provers/Arith/fast_lin_arith.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	26	use "~~/src/Provers/Arith/cancel_sums.ML";
7072 c3f3fd86e11c new simprocs assoc_fold and combine_coeff paulson parents: 7032 diff changeset	27	use "~~/src/Provers/Arith/assoc_fold.ML";
6260 a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	28	use "~~/src/Provers/quantifier1.ML";
18482 ac8456b4080c added Provers/project_rule.ML wenzelm parents: 18449 diff changeset	29	use "~~/src/Provers/project_rule.ML";
8736 0bfd6678a5fa new simprocs for numerals of type "nat" paulson parents: 7739 diff changeset	30	use "~~/src/Provers/Arith/cancel_numerals.ML";
8775 626274171eab combine_numerals replaces both fold_Suc and combine_coeff paulson parents: 8757 diff changeset	31	use "~~/src/Provers/Arith/combine_numerals.ML";
10535 c00b1d0d46ac new simproc file cancel_numeral_factor.ML paulson parents: 10275 diff changeset	32	use "~~/src/Provers/Arith/cancel_numeral_factor.ML";
10689 5c44de6aadf4 loads the new simproc extract_common_term paulson parents: 10535 diff changeset	33	use "~~/src/Provers/Arith/extract_common_term.ML";
13517 42efec18f5b2 Added div+mod cancelling simproc nipkow parents: 13403 diff changeset	34	use "~~/src/Provers/Arith/cancel_div_mod.ML";
15103 79846e8792eb New transitivity reasoners for transitivity only and quasi orders. ballarin parents: 14398 diff changeset	35	use "~~/src/Provers/quasi.ML";
14398 c5c47703f763 Efficient, graph-based reasoner for linear and partial orders. ballarin parents: 14387 diff changeset	36	use "~~/src/Provers/order.ML";
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	37
7703 6b3424e877bd proper dependencies of all theories and packages; wenzelm parents: 7548 diff changeset	38	with_path "Integ" use_thy "Main";
10275 558f7569026e tuned; wenzelm parents: 10263 diff changeset	39
21246 e0e555b67fe5 added structure Main (from Main.ML); wenzelm parents: 19835 diff changeset	40	structure Main =
e0e555b67fe5 added structure Main (from Main.ML); wenzelm parents: 19835 diff changeset	41	struct
e0e555b67fe5 added structure Main (from Main.ML); wenzelm parents: 19835 diff changeset	42	val thy = theory "Main"
e0e555b67fe5 added structure Main (from Main.ML); wenzelm parents: 19835 diff changeset	43	end;
e0e555b67fe5 added structure Main (from Main.ML); wenzelm parents: 19835 diff changeset	44
10263 9cc180732945 path_add "~~/src/HOL/Library"; wenzelm parents: 9891 diff changeset	45	path_add "~~/src/HOL/Library";
5124 1ce3cccfacdb stepping stones: Recdef, Main; wenzelm parents: 5110 diff changeset	46
5501 a63e0c326e6c new files in Integ paulson parents: 5425 diff changeset	47	Goal "True"; (leave subgoal package empty)
13403 bc2b32ee62fd Added theory for setting up program extraction. berghofe parents: 11868 diff changeset	48
bc2b32ee62fd Added theory for setting up program extraction. berghofe parents: 11868 diff changeset	49	val HOL_proofs = !proofs;

author	berghofe
	Mon, 27 Nov 2006 12:11:20 +0100
changeset 21542	4462ee172ef0
parent 21246	e0e555b67fe5
child 21909	a6439243512b
permissions	-rw-r--r--