src/HOLCF/ROOT.ML
author wenzelm
Sat Nov 03 18:41:28 2001 +0100 (2001-11-03)
changeset 12036 49f6c49454c2
parent 6349 f7750d816c21
child 14535 7cb26928e70d
permissions -rw-r--r--
GPLed;
     1 (*  Title:      HOLCF/ROOT.ML
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Conservative (semantic) extension of HOL by the LCF logic.
     7 *)
     8 
     9 val banner = "HOLCF";
    10 writeln banner;
    11 
    12 print_depth 1;
    13 
    14 use_thy "HOLCF";
    15 
    16 use "holcf_logic.ML";
    17 use "cont_consts.ML";
    18 
    19 (* domain package *)
    20 use "domain/library.ML";
    21 use "domain/syntax.ML";
    22 use "domain/axioms.ML";
    23 use "domain/theorems.ML";
    24 use "domain/extender.ML";
    25 use "domain/interface.ML";
    26 
    27 print_depth 10;