src/HOLCF/ROOT.ML
changeset 4008 2444085532c6
parent 3953 473ea5ce5ca8
child 4010 59cac65fb751
     1.1 --- a/src/HOLCF/ROOT.ML	Mon Oct 27 10:46:36 1997 +0100
     1.2 +++ b/src/HOLCF/ROOT.ML	Mon Oct 27 11:34:33 1997 +0100
     1.3 @@ -16,7 +16,6 @@
     1.4  
     1.5  use_thy "HOLCF";
     1.6  
     1.7 -
     1.8  (* sections axioms, ops *)
     1.9  
    1.10  use "ax_ops/holcflogic.ML";
    1.11 @@ -24,7 +23,6 @@
    1.12  use "ax_ops/thy_ops.ML";
    1.13  use "ax_ops/thy_syntax.ML";
    1.14  
    1.15 -
    1.16  (* sections domain, generated *)
    1.17  
    1.18  use "domain/library.ML";
    1.19 @@ -34,7 +32,6 @@
    1.20  use "domain/extender.ML";
    1.21  use "domain/interface.ML";
    1.22  
    1.23 -
    1.24  print_depth 10;  
    1.25  
    1.26  val HOLCF_build_completed = (); (*indicate successful build*)