author | wenzelm |
Fri, 17 Nov 2000 18:49:09 +0100 | |
changeset 10484 | 1f7c944443fc |
parent 9888 | c5622848bf18 |
child 11674 | c67d5ed31417 |
permissions | -rw-r--r-- |
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6349
diff
changeset
|
1 |
(* Title: FOL/ROOT.ML |
0 | 2 |
ID: $Id$ |
1459 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6349
diff
changeset
|
6 |
First-Order Logic. |
0 | 7 |
*) |
8 |
||
9 |
val banner = "First-Order Logic with Natural Deduction"; |
|
10 |
||
11 |
writeln banner; |
|
12 |
||
13 |
print_depth 1; |
|
14 |
||
6260 | 15 |
use "~~/src/Provers/simplifier.ML"; |
16 |
use "~~/src/Provers/splitter.ML"; |
|
17 |
use "~~/src/Provers/ind.ML"; |
|
18 |
use "~~/src/Provers/hypsubst.ML"; |
|
9888 | 19 |
use "~~/src/Provers/rulify.ML"; |
9157 | 20 |
use "~~/src/Provers/make_elim.ML"; |
6260 | 21 |
use "~~/src/Provers/classical.ML"; |
22 |
use "~~/src/Provers/blast.ML"; |
|
23 |
use "~~/src/Provers/clasimp.ML"; |
|
24 |
use "~~/src/Provers/quantifier1.ML"; |
|
0 | 25 |
|
2469 | 26 |
use_thy "FOL"; |
0 | 27 |
|
28 |
print_depth 8; |