author | wenzelm |
Tue, 17 Aug 1999 22:11:05 +0200 | |
changeset 7237 | 2919daadba91 |
parent 7142 | 89e0ff71d113 |
child 7357 | d0e16da40ea2 |
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 |
||
6 |
Adds Classical Higher-order Logic to a database containing Pure Isabelle. |
|
7 |
Should be executed in the subdirectory HOL. |
|
8 |
*) |
|
9 |
||
3947 | 10 |
val banner = "Higher-Order Logic"; |
923 | 11 |
writeln banner; |
12 |
||
13 |
print_depth 1; |
|
14 |
||
6392 | 15 |
(*old-style theory syntax*) |
6260 | 16 |
use "~~/src/Pure/section_utils.ML"; |
923 | 17 |
use "thy_syntax.ML"; |
18 |
||
6260 | 19 |
use "~~/src/Provers/simplifier.ML"; |
20 |
use "~~/src/Provers/split_paired_all.ML"; |
|
21 |
use "~~/src/Provers/splitter.ML"; |
|
22 |
use "~~/src/Provers/hypsubst.ML"; |
|
23 |
use "~~/src/Provers/classical.ML"; |
|
24 |
use "~~/src/Provers/blast.ML"; |
|
25 |
use "~~/src/Provers/clasimp.ML"; |
|
26 |
use "~~/src/Provers/Arith/fast_lin_arith.ML"; |
|
27 |
use "~~/src/Provers/Arith/cancel_sums.ML"; |
|
28 |
use "~~/src/Provers/Arith/cancel_factor.ML"; |
|
29 |
use "~~/src/Provers/Arith/abel_cancel.ML"; |
|
7072 | 30 |
use "~~/src/Provers/Arith/assoc_fold.ML"; |
6260 | 31 |
use "~~/src/Provers/quantifier1.ML"; |
923 | 32 |
|
1338 | 33 |
use_thy "HOL"; |
4088 | 34 |
use "hologic.ML"; |
7072 | 35 |
use "~~/src/Provers/Arith/combine_coeff.ML"; |
4088 | 36 |
use "cladata.ML"; |
37 |
use "simpdata.ML"; |
|
38 |
||
923 | 39 |
use_thy "Ord"; |
40 |
use_thy "subset"; |
|
4864 | 41 |
use "Tools/typedef_package.ML"; |
5105 | 42 |
use_thy "Sum"; |
43 |
use_thy "Gfp"; |
|
923 | 44 |
|
5183 | 45 |
use_thy "NatDef"; |
4296 | 46 |
|
5097 | 47 |
use "Tools/inductive_package.ML"; |
5105 | 48 |
use_thy "Inductive"; |
923 | 49 |
|
5183 | 50 |
use "Tools/datatype_aux.ML"; |
51 |
use "Tools/datatype_prop.ML"; |
|
52 |
use "Tools/datatype_rep_proofs.ML"; |
|
53 |
use "Tools/datatype_abs_proofs.ML"; |
|
54 |
use "Tools/datatype_package.ML"; |
|
55 |
use "Tools/primrec_package.ML"; |
|
5560 | 56 |
use_thy "Datatype"; |
6907 | 57 |
use_thy "Numeral"; |
5183 | 58 |
|
5699 | 59 |
use "Tools/record_package.ML"; |
60 |
use_thy "Record"; |
|
61 |
||
6440 | 62 |
(*TFL: recursive function definitions*) |
63 |
use_thy "WF_Rel"; |
|
64 |
cd "../TFL"; |
|
65 |
use "sys.sml"; |
|
66 |
cd "../HOL"; |
|
67 |
use "Tools/recdef_package.ML"; |
|
68 |
use "Tools/induct_method.ML"; |
|
5425 | 69 |
use_thy "Recdef"; |
923 | 70 |
|
5107
2edf5dfb02f3
Replaced "use_dir" command by "use", because nested calls
berghofe
parents:
5105
diff
changeset
|
71 |
cd "Integ"; |
5501 | 72 |
use_thy "IntDef"; |
5560 | 73 |
use "simproc.ML"; |
7032 | 74 |
use_thy "NatBin"; |
7072 | 75 |
use "bin_simprocs.ML"; |
5107
2edf5dfb02f3
Replaced "use_dir" command by "use", because nested calls
berghofe
parents:
5105
diff
changeset
|
76 |
cd ".."; |
5078 | 77 |
|
5124 | 78 |
(*the all-in-one theory*) |
79 |
use_thy "Main"; |
|
80 |
||
923 | 81 |
print_depth 8; |
82 |
||
5501 | 83 |
Goal "True"; (*leave subgoal package empty*) |