author  nipkow 
Tue, 21 Sep 1999 14:13:45 +0200  
changeset 7548  9e29a3af64ab 
parent 7370  6407a09ac58f 
child 7703  6b3424e877bd 
permissions  rwrr 
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 Higherorder Logic to a database containing Pure Isabelle. 

7 
Should be executed in the subdirectory HOL. 

8 
*) 

9 

3947  10 
val banner = "HigherOrder Logic"; 
923  11 
writeln banner; 
12 

13 
print_depth 1; 

14 

6392  15 
(*oldstyle theory syntax*) 
6260  16 
use "~~/src/Pure/section_utils.ML"; 
923  17 
use "thy_syntax.ML"; 
7370  18 

7357  19 
use "hologic.ML"; 
923  20 

6260  21 
use "~~/src/Provers/simplifier.ML"; 
22 
use "~~/src/Provers/split_paired_all.ML"; 

23 
use "~~/src/Provers/splitter.ML"; 

24 
use "~~/src/Provers/hypsubst.ML"; 

25 
use "~~/src/Provers/classical.ML"; 

26 
use "~~/src/Provers/blast.ML"; 

27 
use "~~/src/Provers/clasimp.ML"; 

28 
use "~~/src/Provers/Arith/fast_lin_arith.ML"; 

29 
use "~~/src/Provers/Arith/cancel_sums.ML"; 

30 
use "~~/src/Provers/Arith/cancel_factor.ML"; 

31 
use "~~/src/Provers/Arith/abel_cancel.ML"; 

7072  32 
use "~~/src/Provers/Arith/assoc_fold.ML"; 
6260  33 
use "~~/src/Provers/quantifier1.ML"; 
7357  34 
use "~~/src/Provers/Arith/combine_coeff.ML"; 
923  35 

36 
use_thy "subset"; 

4864  37 
use "Tools/typedef_package.ML"; 
7357  38 
use_thy "Inductive"; 
5183  39 
use_thy "NatDef"; 
4296  40 

5183  41 
use "Tools/datatype_aux.ML"; 
42 
use "Tools/datatype_prop.ML"; 

43 
use "Tools/datatype_rep_proofs.ML"; 

44 
use "Tools/datatype_abs_proofs.ML"; 

45 
use "Tools/datatype_package.ML"; 

46 
use "Tools/primrec_package.ML"; 

5560  47 
use_thy "Datatype"; 
5699  48 

6440  49 
(*TFL: recursive function definitions*) 
50 
use_thy "WF_Rel"; 

7357  51 
cd "../TFL"; use "sys.sml"; cd "../HOL"; 
5425  52 
use_thy "Recdef"; 
923  53 

7357  54 
use_thy "Numeral"; 
5107
2edf5dfb02f3
Replaced "use_dir" command by "use", because nested calls
berghofe
parents:
5105
diff
changeset

55 
cd "Integ"; 
5501  56 
use_thy "IntDef"; 
5560  57 
use "simproc.ML"; 
7032  58 
use_thy "NatBin"; 
5107
2edf5dfb02f3
Replaced "use_dir" command by "use", because nested calls
berghofe
parents:
5105
diff
changeset

59 
cd ".."; 
5078  60 

5124  61 
(*the allinone theory*) 
62 
use_thy "Main"; 

63 

923  64 
print_depth 8; 
65 

5501  66 
Goal "True"; (*leave subgoal package empty*) 