src/HOLCF/ROOT.ML

 
 print_depth 1;
 
 use_thy "HOLCF";
 
-
 (* sections axioms, ops *)
 
 use "ax_ops/holcflogic.ML";
 use "ax_ops/thy_axioms.ML";
 use "ax_ops/thy_ops.ML";
 use "ax_ops/thy_syntax.ML";
-
 
 (* sections domain, generated *)
 
 use "domain/library.ML";
 use "domain/syntax.ML";
 use "domain/axioms.ML";
 use "domain/theorems.ML";
 use "domain/extender.ML";
 use "domain/interface.ML";
 
-
 print_depth 10;  
 
 val HOLCF_build_completed = (); (*indicate successful build*)