author | wenzelm |
Wed, 08 Nov 2006 13:48:29 +0100 | |
changeset 21243 | afffe1f72143 |
parent 19835 | 81d6dc597559 |
child 21246 | e0e555b67fe5 |
permissions | -rw-r--r-- |
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1165
diff
changeset
|
1 |
(* Title: HOL/ROOT.ML |
923 | 2 |
ID: $Id$ |
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
||
7739 | 6 |
Classical Higher-order Logic. |
923 | 7 |
*) |
8 |
||
3947 | 9 |
val banner = "Higher-Order Logic"; |
923 | 10 |
writeln banner; |
11 |
||
7357 | 12 |
use "hologic.ML"; |
923 | 13 |
|
6260 | 14 |
use "~~/src/Provers/splitter.ML"; |
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 | 20 |
use "~~/src/Provers/eqsubst.ML"; |
11685 | 21 |
use "~~/src/Provers/induct_method.ML"; |
6260 | 22 |
use "~~/src/Provers/classical.ML"; |
23 |
use "~~/src/Provers/blast.ML"; |
|
24 |
use "~~/src/Provers/clasimp.ML"; |
|
25 |
use "~~/src/Provers/Arith/fast_lin_arith.ML"; |
|
26 |
use "~~/src/Provers/Arith/cancel_sums.ML"; |
|
7072 | 27 |
use "~~/src/Provers/Arith/assoc_fold.ML"; |
6260 | 28 |
use "~~/src/Provers/quantifier1.ML"; |
18482 | 29 |
use "~~/src/Provers/project_rule.ML"; |
8736 | 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 | 32 |
use "~~/src/Provers/Arith/cancel_numeral_factor.ML"; |
10689 | 33 |
use "~~/src/Provers/Arith/extract_common_term.ML"; |
13517 | 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 | 37 |
|
7703 | 38 |
with_path "Integ" use_thy "Main"; |
10275 | 39 |
|
10263 | 40 |
path_add "~~/src/HOL/Library"; |
5124 | 41 |
|
5501 | 42 |
Goal "True"; (*leave subgoal package empty*) |
13403 | 43 |
|
44 |
val HOL_proofs = !proofs; |