src/HOLCF/ROOT.ML
changeset 1168 74be52691d62
parent 961 932784dfa671
child 1267 bca91b4e1710
     1.1 --- a/src/HOLCF/ROOT.ML	Thu Jun 29 16:16:24 1995 +0200
     1.2 +++ b/src/HOLCF/ROOT.ML	Thu Jun 29 16:28:40 1995 +0200
     1.3 @@ -7,12 +7,13 @@
     1.4  Should be executed in subdirectory HOLCF.
     1.5  *)
     1.6  
     1.7 -val banner = "Higher-order Logic of Computable Functions";
     1.8 +val banner = "Higher-order Logic of Computable Functions; curried version";
     1.9  writeln banner;
    1.10  print_depth 1;
    1.11  
    1.12  init_thy_reader();
    1.13  
    1.14 +
    1.15  use_thy "Holcfb";
    1.16  use_thy "Void";
    1.17  
    1.18 @@ -63,6 +64,7 @@
    1.19  
    1.20  use_thy "Stream";
    1.21  use_thy "Stream2";
    1.22 +
    1.23  use_thy "Dlist";
    1.24  
    1.25  use "../Pure/install_pp.ML";