src/HOLCF/ROOT.ML
author oheimb
Fri Dec 13 18:45:58 1996 +0100 (1996-12-13)
changeset 2394 91d8abf108be
parent 2353 7405e3cac88a
child 3511 da4dd8b7ced4
permissions -rw-r--r--
adaptions for symbol font
clasohm@1461
     1
(*  Title:      HOLCF/ROOT
nipkow@243
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Franz Regensburger
clasohm@1461
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@243
     5
nipkow@243
     6
ROOT file for the conservative extension of HOL by the LCF logic.
nipkow@243
     7
Should be executed in subdirectory HOLCF.
nipkow@243
     8
*)
nipkow@243
     9
regensbu@1274
    10
val banner = "HOLCF with sections axioms,ops,domain,generated";
oheimb@2394
    11
writeln banner;
regensbu@1274
    12
nipkow@243
    13
print_depth 1;
nipkow@243
    14
regensbu@1274
    15
use_thy "HOLCF";
regensbu@1274
    16
regensbu@1274
    17
(* install sections: axioms, ops *)
regensbu@1274
    18
regensbu@1274
    19
use "ax_ops/holcflogic.ML";
regensbu@1274
    20
use "ax_ops/thy_axioms.ML";
regensbu@1274
    21
use "ax_ops/thy_ops.ML";
regensbu@1274
    22
use "ax_ops/thy_syntax.ML";
regensbu@1274
    23
regensbu@1274
    24
regensbu@1274
    25
(* install sections: domain, generated *)
nipkow@243
    26
regensbu@1285
    27
use "domain/library.ML";
regensbu@1285
    28
use "domain/syntax.ML";
regensbu@1285
    29
use "domain/axioms.ML";
regensbu@1285
    30
use "domain/theorems.ML";
regensbu@1285
    31
use "domain/extender.ML";
regensbu@1285
    32
use "domain/interface.ML";
nipkow@297
    33
regensbu@1274
    34
init_thy_reader();
regensbu@1274
    35
init_pps ();
regensbu@1274
    36
sandnerr@2353
    37
fun qed_spec_mp name =
sandnerr@2353
    38
  let val thm = normalize_thm [RSspec,RSmp] (result())
sandnerr@2353
    39
  in bind_thm(name, thm) end;
sandnerr@2353
    40
oheimb@2394
    41
print_depth 10;  
oheimb@2394
    42
clasohm@1461
    43
val HOLCF_build_completed = (); (*indicate successful build*)