src/HOL/ROOT.ML
author wenzelm
Wed, 14 Apr 1999 19:07:04 +0200
changeset 6431 a42bdc45130d
parent 6392 e2ecfd8622ae
child 6440 7c59a55bae94
permissions -rw-r--r--
Tools/inductive_package.ML;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1264
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 1165
diff changeset
     1
(*  Title:      HOL/ROOT.ML
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     3
    Author:     Tobias Nipkow
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     6
Adds Classical Higher-order Logic to a database containing Pure Isabelle.
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
Should be executed in the subdirectory HOL.
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     8
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     9
3947
eb707467f8c5 adapted to qualified names;
wenzelm
parents: 3578
diff changeset
    10
val banner = "Higher-Order Logic";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    11
writeln banner;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    12
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    13
print_depth 1;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    14
6392
wenzelm
parents: 6349
diff changeset
    15
(*old-style theory syntax*)
6260
wenzelm
parents: 5983
diff changeset
    16
use "~~/src/Pure/section_utils.ML";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    17
use "thy_syntax.ML";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    18
6260
wenzelm
parents: 5983
diff changeset
    19
use "~~/src/Provers/simplifier.ML";
wenzelm
parents: 5983
diff changeset
    20
use "~~/src/Provers/split_paired_all.ML";
wenzelm
parents: 5983
diff changeset
    21
use "~~/src/Provers/splitter.ML";
wenzelm
parents: 5983
diff changeset
    22
use "~~/src/Provers/hypsubst.ML";
wenzelm
parents: 5983
diff changeset
    23
use "~~/src/Provers/classical.ML";
wenzelm
parents: 5983
diff changeset
    24
use "~~/src/Provers/blast.ML";
wenzelm
parents: 5983
diff changeset
    25
use "~~/src/Provers/clasimp.ML";
wenzelm
parents: 5983
diff changeset
    26
use "~~/src/Provers/Arith/fast_lin_arith.ML";
wenzelm
parents: 5983
diff changeset
    27
use "~~/src/Provers/Arith/cancel_sums.ML";
wenzelm
parents: 5983
diff changeset
    28
use "~~/src/Provers/Arith/cancel_factor.ML";
wenzelm
parents: 5983
diff changeset
    29
use "~~/src/Provers/Arith/abel_cancel.ML";
wenzelm
parents: 5983
diff changeset
    30
use "~~/src/Provers/quantifier1.ML";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    31
1338
d2fc3bfaee7f changed simpset of "HOL"
clasohm
parents: 1301
diff changeset
    32
use_thy "HOL";
4088
9be9e39fd862 added thy_data;
wenzelm
parents: 4024
diff changeset
    33
use "hologic.ML";
9be9e39fd862 added thy_data;
wenzelm
parents: 4024
diff changeset
    34
use "cladata.ML";
9be9e39fd862 added thy_data;
wenzelm
parents: 4024
diff changeset
    35
use "simpdata.ML";
9be9e39fd862 added thy_data;
wenzelm
parents: 4024
diff changeset
    36
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    37
use_thy "Ord";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    38
use_thy "subset";
4864
3abfe2093aa0 removed typedef.ML, record.ML;
wenzelm
parents: 4758
diff changeset
    39
use "Tools/typedef_package.ML";
5105
0ff5bec04d02 tuned Inductive.thy;
wenzelm
parents: 5097
diff changeset
    40
use_thy "Sum";
0ff5bec04d02 tuned Inductive.thy;
wenzelm
parents: 5097
diff changeset
    41
use_thy "Gfp";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    42
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5124
diff changeset
    43
use_thy "NatDef";
4296
aa84d9c62454 added Arith provers;
wenzelm
parents: 4222
diff changeset
    44
5097
6c4a7ad6ebc7 Adapted to new inductive definition package.
berghofe
parents: 5078
diff changeset
    45
use "Tools/inductive_package.ML";
5105
0ff5bec04d02 tuned Inductive.thy;
wenzelm
parents: 5097
diff changeset
    46
use_thy "Inductive";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    47
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5124
diff changeset
    48
use "Tools/datatype_aux.ML";
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5124
diff changeset
    49
use "Tools/datatype_prop.ML";
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5124
diff changeset
    50
use "Tools/datatype_rep_proofs.ML";
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5124
diff changeset
    51
use "Tools/datatype_abs_proofs.ML";
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5124
diff changeset
    52
use "Tools/datatype_package.ML";
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5124
diff changeset
    53
use "Tools/primrec_package.ML";
5560
wenzelm
parents: 5501
diff changeset
    54
use_thy "Datatype";
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5124
diff changeset
    55
5699
5b9a359e083c split_paired_all.ML;
wenzelm
parents: 5606
diff changeset
    56
use "Tools/record_package.ML";
5b9a359e083c split_paired_all.ML;
wenzelm
parents: 5606
diff changeset
    57
use_thy "Record";
5b9a359e083c split_paired_all.ML;
wenzelm
parents: 5606
diff changeset
    58
5425
157c6663dedd Added function upto to List.
nipkow
parents: 5298
diff changeset
    59
use_thy "Recdef";
157c6663dedd Added function upto to List.
nipkow
parents: 5298
diff changeset
    60
(*TFL: recursive function definitions*)
6260
wenzelm
parents: 5983
diff changeset
    61
cd "~~/src/TFL";
5425
157c6663dedd Added function upto to List.
nipkow
parents: 5298
diff changeset
    62
use "sys.sml";
6260
wenzelm
parents: 5983
diff changeset
    63
cd "~~/src/HOL";
6431
a42bdc45130d Tools/inductive_package.ML;
wenzelm
parents: 6392
diff changeset
    64
use "Tools/recdef_package.ML";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    65
5107
2edf5dfb02f3 Replaced "use_dir" command by "use", because nested calls
berghofe
parents: 5105
diff changeset
    66
cd "Integ";
5501
a63e0c326e6c new files in Integ
paulson
parents: 5425
diff changeset
    67
use_thy "IntDef";
5560
wenzelm
parents: 5501
diff changeset
    68
use "simproc.ML";
5110
2497807020fa fixed Integ;
wenzelm
parents: 5107
diff changeset
    69
use_thy "Bin";
5107
2edf5dfb02f3 Replaced "use_dir" command by "use", because nested calls
berghofe
parents: 5105
diff changeset
    70
cd "..";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents: 4896
diff changeset
    71
5124
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents: 5110
diff changeset
    72
(*the all-in-one theory*)
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents: 5110
diff changeset
    73
use_thy "Main";
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents: 5110
diff changeset
    74
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    75
print_depth 8;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    76
5501
a63e0c326e6c new files in Integ
paulson
parents: 5425
diff changeset
    77
Goal "True";  (*leave subgoal package empty*)