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
     1 (*  Title:      HOLCF/ROOT
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 ROOT file for the conservative extension of HOL by the LCF logic.
     7 Should be executed in subdirectory HOLCF.
     8 *)
     9 
    10 val banner = "HOLCF with sections axioms,ops,domain,generated";
    11 writeln banner;
    12 
    13 print_depth 1;
    14 
    15 use_thy "HOLCF";
    16 
    17 (* install sections: axioms, ops *)
    18 
    19 use "ax_ops/holcflogic.ML";
    20 use "ax_ops/thy_axioms.ML";
    21 use "ax_ops/thy_ops.ML";
    22 use "ax_ops/thy_syntax.ML";
    23 
    24 
    25 (* install sections: domain, generated *)
    26 
    27 use "domain/library.ML";
    28 use "domain/syntax.ML";
    29 use "domain/axioms.ML";
    30 use "domain/theorems.ML";
    31 use "domain/extender.ML";
    32 use "domain/interface.ML";
    33 
    34 init_thy_reader();
    35 init_pps ();
    36 
    37 fun qed_spec_mp name =
    38   let val thm = normalize_thm [RSspec,RSmp] (result())
    39   in bind_thm(name, thm) end;
    40 
    41 print_depth 10;  
    42 
    43 val HOLCF_build_completed = (); (*indicate successful build*)