src/HOLCF/ROOT.ML
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 14535 7cb26928e70d
child 15188 9d57263faf9e
permissions -rw-r--r--
Merged in license change from Isabelle2004
     1 (*  Title:      HOLCF/ROOT.ML
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4 
     5 Conservative (semantic) extension of HOL by the LCF logic.
     6 *)
     7 
     8 val banner = "HOLCF";
     9 writeln banner;
    10 
    11 print_depth 1;
    12 
    13 use_thy "HOLCF";
    14 
    15 use "holcf_logic.ML";
    16 use "cont_consts.ML";
    17 
    18 (* domain package *)
    19 use "domain/library.ML";
    20 use "domain/syntax.ML";
    21 use "domain/axioms.ML";
    22 use "domain/theorems.ML";
    23 use "domain/extender.ML";
    24 use "domain/interface.ML";
    25 
    26 path_add "~~/src/HOLCF/ex";
    27 use_thy "Streams";
    28 
    29 print_depth 10;