isabelle: src/HOL/ROOT.ML@6b3424e877bd (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";
7370 6407a09ac58f tuned; wenzelm parents: 7357 diff changeset	18
7357 d0e16da40ea2 proper bootstrap of HOL theory and packages; wenzelm parents: 7237 diff changeset	19	use "hologic.ML";
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	20
6260 a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	21	use "~~/src/Provers/simplifier.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	22	use "~~/src/Provers/split_paired_all.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	23	use "~~/src/Provers/splitter.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	24	use "~~/src/Provers/hypsubst.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	25	use "~~/src/Provers/classical.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	26	use "~~/src/Provers/blast.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	27	use "~~/src/Provers/clasimp.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	28	use "~~/src/Provers/Arith/fast_lin_arith.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	29	use "~~/src/Provers/Arith/cancel_sums.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	30	use "~~/src/Provers/Arith/cancel_factor.ML";
a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	31	use "~~/src/Provers/Arith/abel_cancel.ML";
7072 c3f3fd86e11c new simprocs assoc_fold and combine_coeff paulson parents: 7032 diff changeset	32	use "~~/src/Provers/Arith/assoc_fold.ML";
6260 a8010d459ef7 ~~; wenzelm parents: 5983 diff changeset	33	use "~~/src/Provers/quantifier1.ML";
7357 d0e16da40ea2 proper bootstrap of HOL theory and packages; wenzelm parents: 7237 diff changeset	34	use "~~/src/Provers/Arith/combine_coeff.ML";
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	35
7703 6b3424e877bd proper dependencies of all theories and packages; wenzelm parents: 7548 diff changeset	36	with_path "Integ" use_thy "Main";
5124 1ce3cccfacdb stepping stones: Recdef, Main; wenzelm parents: 5110 diff changeset	37
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	38	print_depth 8;
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	39
5501 a63e0c326e6c new files in Integ paulson parents: 5425 diff changeset	40	Goal "True"; (leave subgoal package empty)

author	wenzelm
	Mon, 04 Oct 1999 21:45:10 +0200
changeset 7703	6b3424e877bd
parent 7548	9e29a3af64ab
child 7739	bfe45b716dfc
permissions	-rw-r--r--