author | wenzelm |
Fri, 25 Jul 1997 13:18:45 +0200 | |
changeset 3578 | b2b9a9ddb9cc |
parent 3511 | da4dd8b7ced4 |
child 3947 | eb707467f8c5 |
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 |
||
10 |
val banner = "Higher-Order Logic with curried functions"; |
|
11 |
writeln banner; |
|
12 |
||
13 |
print_depth 1; |
|
14 |
||
15 |
(* Add user sections *) |
|
16 |
use "../Pure/section_utils.ML"; |
|
17 |
use "thy_syntax.ML"; |
|
18 |
||
3578 | 19 |
use "../Provers/simplifier.ML"; |
1024 | 20 |
use "../Provers/splitter.ML"; |
923 | 21 |
use "../Provers/hypsubst.ML"; |
22 |
use "../Provers/classical.ML"; |
|
2857 | 23 |
use "../Provers/blast.ML"; |
2115 | 24 |
use "../Provers/nat_transitive.ML"; |
923 | 25 |
|
26 |
||
1338 | 27 |
use_thy "HOL"; |
923 | 28 |
use_thy "Ord"; |
29 |
use_thy "subset"; |
|
1470 | 30 |
use "typedef.ML"; |
923 | 31 |
use_thy "Sum"; |
32 |
use_thy "Gfp"; |
|
33 |
||
34 |
use "datatype.ML"; |
|
35 |
use "ind_syntax.ML"; |
|
36 |
use "add_ind_def.ML"; |
|
37 |
use "intr_elim.ML"; |
|
38 |
use "indrule.ML"; |
|
39 |
use_thy "Inductive"; |
|
40 |
||
1515 | 41 |
use_thy "RelPow"; |
923 | 42 |
use_thy "Finite"; |
43 |
use_thy "Sexp"; |
|
2019 | 44 |
use_thy "Option"; |
3195 | 45 |
use_thy "WF_Rel"; |
923 | 46 |
use_thy "List"; |
47 |
||
3195 | 48 |
(*TFL: recursive function definitions*) |
49 |
cd "../TFL"; |
|
50 |
use "sys.sml"; |
|
51 |
cd "../HOL"; |
|
52 |
||
923 | 53 |
print_depth 8; |
54 |
||
1165 | 55 |
val HOL_build_completed = (); (*indicate successful build*) |