src/HOLCF/ROOT.ML
changeset 243 c22b85994e17
child 297 5ef75ff3baeb
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/ROOT.ML	Wed Jan 19 17:35:01 1994 +0100
     1.3 @@ -0,0 +1,68 @@
     1.4 +(*  Title:	HOLCF/ROOT
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Franz Regensburger
     1.7 +    Copyright	1993 Technische Universitaet Muenchen
     1.8 +
     1.9 +ROOT file for the conservative extension of HOL by the LCF logic.
    1.10 +Should be executed in subdirectory HOLCF.
    1.11 +*)
    1.12 +
    1.13 +val banner = "Higher-order Logic of Computable Functions";
    1.14 +writeln banner;
    1.15 +print_depth 1;
    1.16 +
    1.17 +structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
    1.18 +Readthy.loaded_thys := !loaded_thys;
    1.19 +open Readthy;
    1.20 +
    1.21 +use_thy "Holcfb";
    1.22 +use_thy "Void";
    1.23 +use_thy "Porder";
    1.24 +use_thy "Pcpo";
    1.25 +
    1.26 +use_thy "Fun1";
    1.27 +use_thy "Fun2";
    1.28 +use_thy "Fun3";
    1.29 +
    1.30 +use_thy "Cont";
    1.31 +
    1.32 +use_thy "Cfun1";
    1.33 +use_thy "Cfun2";
    1.34 +use_thy "Cfun3";
    1.35 +
    1.36 +use_thy "Cprod1";
    1.37 +use_thy "Cprod2";
    1.38 +use_thy "Cprod3";
    1.39 +
    1.40 +use_thy "Sprod0";
    1.41 +use_thy "Sprod1"; 
    1.42 +use_thy "Sprod2"; 
    1.43 +use_thy "Sprod3"; 
    1.44 +
    1.45 +use_thy "Ssum0";
    1.46 +use_thy "Ssum1";
    1.47 +use_thy "Ssum2";
    1.48 +use_thy "Ssum3";
    1.49 +
    1.50 +use_thy "Lift1";
    1.51 +use_thy "Lift2";
    1.52 +use_thy "Lift3";
    1.53 +
    1.54 +use_thy "Fix";
    1.55 +
    1.56 +use_thy "ccc1";
    1.57 +use_thy "One";
    1.58 +use_thy "Tr1";
    1.59 +use_thy "Tr2";
    1.60 +
    1.61 +use_thy "HOLCF";
    1.62 +
    1.63 +use_thy "Dnat";
    1.64 +use_thy "Dnat2";
    1.65 +use_thy "Stream";
    1.66 +use_thy "Stream2";
    1.67 +
    1.68 +use "../Pure/install_pp.ML";
    1.69 +print_depth 8;  
    1.70 +
    1.71 +val HOLCF_build_completed = ();	(*indicate successful build*)