author | paulson |
Fri, 12 May 2000 15:05:02 +0200 | |
changeset 8862 | 78643f8449c6 |
parent 8812 | 7239b21e2068 |
child 9157 | 998dd2fb5795 |
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 |
||
7739 | 6 |
Classical Higher-order Logic. |
923 | 7 |
*) |
8 |
||
3947 | 9 |
val banner = "Higher-Order Logic"; |
923 | 10 |
writeln banner; |
11 |
||
12 |
print_depth 1; |
|
13 |
||
6392 | 14 |
(*old-style theory syntax*) |
923 | 15 |
use "thy_syntax.ML"; |
7370 | 16 |
|
7357 | 17 |
use "hologic.ML"; |
923 | 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"; |
8736 | 32 |
use "~~/src/Provers/Arith/cancel_numerals.ML"; |
8775
626274171eab
combine_numerals replaces both fold_Suc and combine_coeff
paulson
parents:
8757
diff
changeset
|
33 |
use "~~/src/Provers/Arith/combine_numerals.ML"; |
923 | 34 |
|
7703 | 35 |
with_path "Integ" use_thy "Main"; |
5124 | 36 |
|
923 | 37 |
print_depth 8; |
38 |
||
5501 | 39 |
Goal "True"; (*leave subgoal package empty*) |