author | wenzelm |
Fri, 03 Jul 1998 18:05:03 +0200 | |
changeset 5126 | 01cbf154d926 |
parent 5124 | 1ce3cccfacdb |
child 5183 | 89f162de39cf |
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 |
||
15 |
(* Add user sections *) |
|
4222 | 16 |
use "$ISABELLE_HOME/src/Pure/section_utils.ML"; |
923 | 17 |
use "thy_syntax.ML"; |
18 |
||
4222 | 19 |
use "$ISABELLE_HOME/src/Provers/simplifier.ML"; |
20 |
use "$ISABELLE_HOME/src/Provers/splitter.ML"; |
|
21 |
use "$ISABELLE_HOME/src/Provers/hypsubst.ML"; |
|
22 |
use "$ISABELLE_HOME/src/Provers/classical.ML"; |
|
23 |
use "$ISABELLE_HOME/src/Provers/blast.ML"; |
|
4296 | 24 |
use "$ISABELLE_HOME/src/Provers/Arith/nat_transitive.ML"; |
25 |
use "$ISABELLE_HOME/src/Provers/Arith/cancel_sums.ML"; |
|
26 |
use "$ISABELLE_HOME/src/Provers/Arith/cancel_factor.ML"; |
|
4320
24d9e6639cd4
Moved the quantifier elimination simp procs into Provers.
nipkow
parents:
4296
diff
changeset
|
27 |
use "$ISABELLE_HOME/src/Provers/quantifier1.ML"; |
923 | 28 |
|
4088 | 29 |
use "thy_data.ML"; |
923 | 30 |
|
1338 | 31 |
use_thy "HOL"; |
4088 | 32 |
use "hologic.ML"; |
33 |
use "cladata.ML"; |
|
34 |
use "simpdata.ML"; |
|
35 |
||
923 | 36 |
use_thy "Ord"; |
37 |
use_thy "subset"; |
|
4864 | 38 |
use "Tools/typedef_package.ML"; |
5105 | 39 |
use_thy "Sum"; |
40 |
use_thy "Gfp"; |
|
923 | 41 |
|
4864 | 42 |
use "Tools/record_package.ML"; |
43 |
use_thy "Record"; |
|
4573 | 44 |
|
923 | 45 |
use "datatype.ML"; |
4296 | 46 |
use_thy "Arith"; |
47 |
use "arith_data.ML"; |
|
48 |
||
5097 | 49 |
use "Tools/inductive_package.ML"; |
5105 | 50 |
use_thy "Inductive"; |
923 | 51 |
|
1515 | 52 |
use_thy "RelPow"; |
923 | 53 |
use_thy "Finite"; |
54 |
use_thy "Sexp"; |
|
5124 | 55 |
use_thy "Recdef"; |
3981 | 56 |
use_thy "Map"; |
4896
4727272f3db6
New syntax for function update; moved to main HOL directory
paulson
parents:
4864
diff
changeset
|
57 |
use_thy "Update"; |
923 | 58 |
|
5107
2edf5dfb02f3
Replaced "use_dir" command by "use", because nested calls
berghofe
parents:
5105
diff
changeset
|
59 |
cd "Integ"; |
5110 | 60 |
use_thy "Bin"; |
5107
2edf5dfb02f3
Replaced "use_dir" command by "use", because nested calls
berghofe
parents:
5105
diff
changeset
|
61 |
cd ".."; |
5078 | 62 |
|
3195 | 63 |
(*TFL: recursive function definitions*) |
4517 | 64 |
cd "$ISABELLE_HOME/src/TFL"; |
3195 | 65 |
use "sys.sml"; |
5078 | 66 |
cd "$ISABELLE_HOME/src/HOL"; |
3195 | 67 |
|
5124 | 68 |
(*the all-in-one theory*) |
69 |
use_thy "Main"; |
|
70 |
||
923 | 71 |
print_depth 8; |
72 |
||
1165 | 73 |
val HOL_build_completed = (); (*indicate successful build*) |