src/HOLCF/ROOT.ML
author regensbu
Thu Jun 29 16:28:40 1995 +0200 (1995-06-29)
changeset 1168 74be52691d62
parent 961 932784dfa671
child 1267 bca91b4e1710
permissions -rw-r--r--
The curried version of HOLCF is now just called HOLCF. The old
uncurried version is no longer supported
     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; curried version";
    11 writeln banner;
    12 print_depth 1;
    13 
    14 init_thy_reader();
    15 
    16 
    17 use_thy "Holcfb";
    18 use_thy "Void";
    19 
    20 use_thy "Porder0";
    21 use_thy "Porder";
    22 
    23 use_thy "Pcpo";
    24 
    25 use_thy "Fun1";
    26 use_thy "Fun2";
    27 use_thy "Fun3";
    28 
    29 use_thy "Cont";
    30 
    31 use_thy "Cfun1";
    32 use_thy "Cfun2";
    33 use_thy "Cfun3";
    34 
    35 use_thy "Cprod1";
    36 use_thy "Cprod2";
    37 use_thy "Cprod3";
    38 
    39 use_thy "Sprod0";
    40 use_thy "Sprod1"; 
    41 use_thy "Sprod2"; 
    42 use_thy "Sprod3"; 
    43 
    44 use_thy "Ssum0";
    45 use_thy "Ssum1";
    46 use_thy "Ssum2";
    47 use_thy "Ssum3";
    48 
    49 use_thy "Lift1";
    50 use_thy "Lift2";
    51 use_thy "Lift3";
    52 
    53 use_thy "Fix";
    54 
    55 use_thy "ccc1";
    56 use_thy "One";
    57 use_thy "Tr1";
    58 use_thy "Tr2";
    59  
    60 use_thy "HOLCF";
    61 
    62 use_thy "Dnat";
    63 use_thy "Dnat2";
    64 
    65 use_thy "Stream";
    66 use_thy "Stream2";
    67 
    68 use_thy "Dlist";
    69 
    70 use "../Pure/install_pp.ML";
    71 print_depth 8;  
    72 
    73 val HOLCF_build_completed = ();	(*indicate successful build*)