src/HOLCF/ROOT.ML
author wenzelm
Fri Nov 29 15:31:13 1996 +0100 (1996-11-29)
changeset 2282 90fb68d597f8
parent 2278 d63ffafce255
child 2353 7405e3cac88a
permissions -rw-r--r--
added qed_spec_mp (from HOL);
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";
regensbu@1274
    11
init_thy_reader();
regensbu@1274
    12
wenzelm@2282
    13
fun qed_spec_mp name =
wenzelm@2282
    14
  let val thm = normalize_thm [RSspec,RSmp] (result())
wenzelm@2282
    15
  in bind_thm(name, thm) end;
wenzelm@2282
    16
regensbu@1274
    17
(* start 8bit 1 *)
oheimb@2278
    18
val banner = 
oheimb@2278
    19
        "HOLCF with sections axioms,ops,domain,generated and 8bit characters";
regensbu@1274
    20
(* end 8bit 1 *)
regensbu@1274
    21
nipkow@243
    22
writeln banner;
nipkow@243
    23
print_depth 1;
nipkow@243
    24
regensbu@1274
    25
use_thy "HOLCF";
regensbu@1274
    26
regensbu@1274
    27
(* install sections: axioms, ops *)
regensbu@1274
    28
regensbu@1274
    29
use "ax_ops/holcflogic.ML";
regensbu@1274
    30
use "ax_ops/thy_axioms.ML";
regensbu@1274
    31
use "ax_ops/thy_ops.ML";
regensbu@1274
    32
use "ax_ops/thy_syntax.ML";
regensbu@1274
    33
regensbu@1274
    34
regensbu@1274
    35
(* install sections: domain, generated *)
nipkow@243
    36
regensbu@1285
    37
use "domain/library.ML";
regensbu@1285
    38
use "domain/syntax.ML";
regensbu@1285
    39
use "domain/axioms.ML";
regensbu@1285
    40
use "domain/theorems.ML";
regensbu@1285
    41
use "domain/extender.ML";
regensbu@1285
    42
use "domain/interface.ML";
nipkow@297
    43
regensbu@1274
    44
init_thy_reader();
regensbu@1274
    45
init_pps ();
regensbu@1274
    46
regensbu@1274
    47
print_depth 100;  
regensbu@1571
    48
make_html:=false;
nipkow@243
    49
clasohm@1461
    50
val HOLCF_build_completed = (); (*indicate successful build*)