src/HOLCF/ROOT.ML

 
 ROOT file for the conservative extension of HOL by the LCF logic.
 Should be executed in subdirectory HOLCF.
 *)
 
-val banner = "Higher-order Logic of Computable Functions";
+val banner = "Higher-order Logic of Computable Functions; curried version";
 writeln banner;
 print_depth 1;
 
 init_thy_reader();
+
 
 use_thy "Holcfb";
 use_thy "Void";
 
 use_thy "Porder0";

 use_thy "Dnat";
 use_thy "Dnat2";
 
 use_thy "Stream";
 use_thy "Stream2";
+
 use_thy "Dlist";
 
 use "../Pure/install_pp.ML";
 print_depth 8;