1 (* Title: HOL/ROOT.ML |
1 (* Title: HOL/ROOT.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 |
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Classical Higher-order Logic. |
4 Classical Higher-order Logic. |
7 *) |
5 *) |
8 |
6 |
9 val banner = "Higher-Order Logic"; |
7 use_thy "Main"; |
10 writeln banner; |
|
11 |
|
12 use "hologic.ML"; |
|
13 |
|
14 use "~~/src/Provers/splitter.ML"; |
|
15 use "~~/src/Provers/hypsubst.ML"; |
|
16 use "~~/src/Provers/IsaPlanner/zipper.ML"; |
|
17 use "~~/src/Provers/IsaPlanner/isand.ML"; |
|
18 use "~~/src/Provers/IsaPlanner/rw_tools.ML"; |
|
19 use "~~/src/Provers/IsaPlanner/rw_inst.ML"; |
|
20 use "~~/src/Provers/eqsubst.ML"; |
|
21 use "~~/src/Provers/induct_method.ML"; |
|
22 use "~~/src/Provers/classical.ML"; |
|
23 use "~~/src/Provers/blast.ML"; |
|
24 use "~~/src/Provers/clasimp.ML"; |
|
25 use "~~/src/Pure/General/int.ML"; |
|
26 use "~~/src/Pure/General/rat.ML"; |
|
27 use "~~/src/Provers/Arith/fast_lin_arith.ML"; |
|
28 use "~~/src/Provers/Arith/cancel_sums.ML"; |
|
29 use "~~/src/Provers/quantifier1.ML"; |
|
30 use "~~/src/Provers/project_rule.ML"; |
|
31 use "~~/src/Provers/Arith/cancel_numerals.ML"; |
|
32 use "~~/src/Provers/Arith/combine_numerals.ML"; |
|
33 use "~~/src/Provers/Arith/cancel_numeral_factor.ML"; |
|
34 use "~~/src/Provers/Arith/extract_common_term.ML"; |
|
35 use "~~/src/Provers/quasi.ML"; |
|
36 use "~~/src/Provers/order.ML"; |
|
37 |
|
38 with_path "Integ" use_thy "Main"; |
|
39 |
8 |
40 path_add "~~/src/HOL/Library"; |
9 path_add "~~/src/HOL/Library"; |
41 |
10 |
42 Goal "True"; (*leave subgoal package empty*) |
11 Goal "True"; (*leave subgoal package empty*) |
43 |
|
44 val HOL_proofs = !proofs; |
|