src/HOLCF/ROOT.ML
author nipkow
Wed Jan 19 17:35:01 1994 +0100 (1994-01-19)
changeset 243 c22b85994e17
child 297 5ef75ff3baeb
permissions -rw-r--r--
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
in HOL.
     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 structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
    15 Readthy.loaded_thys := !loaded_thys;
    16 open Readthy;
    17 
    18 use_thy "Holcfb";
    19 use_thy "Void";
    20 use_thy "Porder";
    21 use_thy "Pcpo";
    22 
    23 use_thy "Fun1";
    24 use_thy "Fun2";
    25 use_thy "Fun3";
    26 
    27 use_thy "Cont";
    28 
    29 use_thy "Cfun1";
    30 use_thy "Cfun2";
    31 use_thy "Cfun3";
    32 
    33 use_thy "Cprod1";
    34 use_thy "Cprod2";
    35 use_thy "Cprod3";
    36 
    37 use_thy "Sprod0";
    38 use_thy "Sprod1"; 
    39 use_thy "Sprod2"; 
    40 use_thy "Sprod3"; 
    41 
    42 use_thy "Ssum0";
    43 use_thy "Ssum1";
    44 use_thy "Ssum2";
    45 use_thy "Ssum3";
    46 
    47 use_thy "Lift1";
    48 use_thy "Lift2";
    49 use_thy "Lift3";
    50 
    51 use_thy "Fix";
    52 
    53 use_thy "ccc1";
    54 use_thy "One";
    55 use_thy "Tr1";
    56 use_thy "Tr2";
    57 
    58 use_thy "HOLCF";
    59 
    60 use_thy "Dnat";
    61 use_thy "Dnat2";
    62 use_thy "Stream";
    63 use_thy "Stream2";
    64 
    65 use "../Pure/install_pp.ML";
    66 print_depth 8;  
    67 
    68 val HOLCF_build_completed = ();	(*indicate successful build*)