src/HOL/ROOT.ML
author nipkow
Wed, 02 Sep 1998 16:52:06 +0200
changeset 5425 157c6663dedd
parent 5298 81716d9b2b09
child 5501 a63e0c326e6c
permissions -rw-r--r--
Added function upto to List. Had to rearrange loading sequence because now List uses Recdef.
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
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    15
(* Add user sections *)
4222
d7573d6d0513 refer to $ISABELLE_HOME/src;
wenzelm
parents: 4088
diff changeset
    16
use "$ISABELLE_HOME/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
4222
d7573d6d0513 refer to $ISABELLE_HOME/src;
wenzelm
parents: 4088
diff changeset
    19
use "$ISABELLE_HOME/src/Provers/simplifier.ML";
d7573d6d0513 refer to $ISABELLE_HOME/src;
wenzelm
parents: 4088
diff changeset
    20
use "$ISABELLE_HOME/src/Provers/splitter.ML";
d7573d6d0513 refer to $ISABELLE_HOME/src;
wenzelm
parents: 4088
diff changeset
    21
use "$ISABELLE_HOME/src/Provers/hypsubst.ML";
d7573d6d0513 refer to $ISABELLE_HOME/src;
wenzelm
parents: 4088
diff changeset
    22
use "$ISABELLE_HOME/src/Provers/classical.ML";
d7573d6d0513 refer to $ISABELLE_HOME/src;
wenzelm
parents: 4088
diff changeset
    23
use "$ISABELLE_HOME/src/Provers/blast.ML";
5219
924359415f09 functorized Clasimp module;
wenzelm
parents: 5183
diff changeset
    24
use "$ISABELLE_HOME/src/Provers/clasimp.ML";
4296
aa84d9c62454 added Arith provers;
wenzelm
parents: 4222
diff changeset
    25
use "$ISABELLE_HOME/src/Provers/Arith/nat_transitive.ML";
aa84d9c62454 added Arith provers;
wenzelm
parents: 4222
diff changeset
    26
use "$ISABELLE_HOME/src/Provers/Arith/cancel_sums.ML";
aa84d9c62454 added Arith provers;
wenzelm
parents: 4222
diff changeset
    27
use "$ISABELLE_HOME/src/Provers/Arith/cancel_factor.ML";
4320
24d9e6639cd4 Moved the quantifier elimination simp procs into Provers.
nipkow
parents: 4296
diff changeset
    28
use "$ISABELLE_HOME/src/Provers/quantifier1.ML";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    29
1338
d2fc3bfaee7f changed simpset of "HOL"
clasohm
parents: 1301
diff changeset
    30
use_thy "HOL";
4088
9be9e39fd862 added thy_data;
wenzelm
parents: 4024
diff changeset
    31
use "hologic.ML";
9be9e39fd862 added thy_data;
wenzelm
parents: 4024
diff changeset
    32
use "cladata.ML";
9be9e39fd862 added thy_data;
wenzelm
parents: 4024
diff changeset
    33
use "simpdata.ML";
9be9e39fd862 added thy_data;
wenzelm
parents: 4024
diff changeset
    34
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    35
use_thy "Ord";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    36
use_thy "subset";
4864
3abfe2093aa0 removed typedef.ML, record.ML;
wenzelm
parents: 4758
diff changeset
    37
use "Tools/typedef_package.ML";
5105
0ff5bec04d02 tuned Inductive.thy;
wenzelm
parents: 5097
diff changeset
    38
use_thy "Sum";
0ff5bec04d02 tuned Inductive.thy;
wenzelm
parents: 5097
diff changeset
    39
use_thy "Gfp";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    40
4864
3abfe2093aa0 removed typedef.ML, record.ML;
wenzelm
parents: 4758
diff changeset
    41
use "Tools/record_package.ML";
3abfe2093aa0 removed typedef.ML, record.ML;
wenzelm
parents: 4758
diff changeset
    42
use_thy "Record";
4573
fe504f608835 added record.ML;
wenzelm
parents: 4517
diff changeset
    43
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5124
diff changeset
    44
use_thy "NatDef";
4296
aa84d9c62454 added Arith provers;
wenzelm
parents: 4222
diff changeset
    45
5097
6c4a7ad6ebc7 Adapted to new inductive definition package.
berghofe
parents: 5078
diff changeset
    46
use "Tools/inductive_package.ML";
5105
0ff5bec04d02 tuned Inductive.thy;
wenzelm
parents: 5097
diff changeset
    47
use_thy "Inductive";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    48
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5124
diff changeset
    49
use "Tools/datatype_aux.ML";
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5124
diff changeset
    50
use "Tools/datatype_prop.ML";
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5124
diff changeset
    51
use "Tools/datatype_rep_proofs.ML";
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5124
diff changeset
    52
use "Tools/datatype_abs_proofs.ML";
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5124
diff changeset
    53
use "Tools/datatype_package.ML";
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5124
diff changeset
    54
use "Tools/primrec_package.ML";
5425
157c6663dedd Added function upto to List.
nipkow
parents: 5298
diff changeset
    55
use_thy"Datatype";
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5124
diff changeset
    56
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5124
diff changeset
    57
use_thy "Arith";
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5124
diff changeset
    58
use "arith_data.ML";
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5124
diff changeset
    59
5425
157c6663dedd Added function upto to List.
nipkow
parents: 5298
diff changeset
    60
use_thy "Recdef";
157c6663dedd Added function upto to List.
nipkow
parents: 5298
diff changeset
    61
(*TFL: recursive function definitions*)
157c6663dedd Added function upto to List.
nipkow
parents: 5298
diff changeset
    62
cd "$ISABELLE_HOME/src/TFL";
157c6663dedd Added function upto to List.
nipkow
parents: 5298
diff changeset
    63
use "sys.sml";
157c6663dedd Added function upto to List.
nipkow
parents: 5298
diff changeset
    64
cd "$ISABELLE_HOME/src/HOL";
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";
5110
2497807020fa fixed Integ;
wenzelm
parents: 5107
diff changeset
    67
use_thy "Bin";
5107
2edf5dfb02f3 Replaced "use_dir" command by "use", because nested calls
berghofe
parents: 5105
diff changeset
    68
cd "..";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents: 4896
diff changeset
    69
5124
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents: 5110
diff changeset
    70
(*the all-in-one theory*)
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents: 5110
diff changeset
    71
use_thy "Main";
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents: 5110
diff changeset
    72
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    73
print_depth 8;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    74
1165
97b2bb5d43c3 renamed CHOL to HOL
clasohm
parents: 1024
diff changeset
    75
val HOL_build_completed = ();   (*indicate successful build*)