src/HOLCF/ROOT.ML
author oheimb
Mon Sep 21 22:58:43 1998 +0200 (1998-09-21)
changeset 5517 863f56450888
parent 4129 2fd816aa6206
child 6349 f7750d816c21
permissions -rw-r--r--
added dependance on HOL
     1 (*  Title:      HOLCF/ROOT.ML
     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 HOL_build_completed;    (* Cause HOLCF to fail if HOL did *)
    11 
    12 val banner = "HOLCF";
    13 writeln banner;
    14 
    15 print_depth 1;
    16 
    17 use_thy "HOLCF";
    18 
    19 use "holcf_logic.ML";
    20 use "cont_consts.ML";
    21 
    22 (* domain package *)
    23 use "domain/library.ML";
    24 use "domain/syntax.ML";
    25 use "domain/axioms.ML";
    26 use "domain/theorems.ML";
    27 use "domain/extender.ML";
    28 use "domain/interface.ML";
    29 
    30 print_depth 10;  
    31 
    32 val HOLCF_build_completed = (); (*indicate successful build*)