src/HOLCF/ROOT.ML
author regensbu
Fri Mar 17 15:35:09 1995 +0100 (1995-03-17)
changeset 961 932784dfa671
parent 625 119391dd1d59
child 1168 74be52691d62
permissions -rw-r--r--
Removed bugs which occurred due to new generation mechanism for type variables
     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 = "Higher-order Logic of Computable Functions";
    11 writeln banner;
    12 print_depth 1;
    13 
    14 init_thy_reader();
    15 
    16 use_thy "Holcfb";
    17 use_thy "Void";
    18 
    19 use_thy "Porder0";
    20 use_thy "Porder";
    21 
    22 use_thy "Pcpo";
    23 
    24 use_thy "Fun1";
    25 use_thy "Fun2";
    26 use_thy "Fun3";
    27 
    28 use_thy "Cont";
    29 
    30 use_thy "Cfun1";
    31 use_thy "Cfun2";
    32 use_thy "Cfun3";
    33 
    34 use_thy "Cprod1";
    35 use_thy "Cprod2";
    36 use_thy "Cprod3";
    37 
    38 use_thy "Sprod0";
    39 use_thy "Sprod1"; 
    40 use_thy "Sprod2"; 
    41 use_thy "Sprod3"; 
    42 
    43 use_thy "Ssum0";
    44 use_thy "Ssum1";
    45 use_thy "Ssum2";
    46 use_thy "Ssum3";
    47 
    48 use_thy "Lift1";
    49 use_thy "Lift2";
    50 use_thy "Lift3";
    51 
    52 use_thy "Fix";
    53 
    54 use_thy "ccc1";
    55 use_thy "One";
    56 use_thy "Tr1";
    57 use_thy "Tr2";
    58  
    59 use_thy "HOLCF";
    60 
    61 use_thy "Dnat";
    62 use_thy "Dnat2";
    63 
    64 use_thy "Stream";
    65 use_thy "Stream2";
    66 use_thy "Dlist";
    67 
    68 use "../Pure/install_pp.ML";
    69 print_depth 8;  
    70 
    71 val HOLCF_build_completed = ();	(*indicate successful build*)