src/HOLCF/ROOT.ML
changeset 4122 f63c283cefaf
parent 4041 4df7f385fe9f
child 4128 42584a53a3e7
     1.1 --- a/src/HOLCF/ROOT.ML	Tue Nov 04 14:37:51 1997 +0100
     1.2 +++ b/src/HOLCF/ROOT.ML	Tue Nov 04 14:40:29 1997 +0100
     1.3 @@ -14,14 +14,10 @@
     1.4  
     1.5  use_thy "HOLCF";
     1.6  
     1.7 -(* sections axioms, ops *)
     1.8 -use "ax_ops/holcflogic.ML";
     1.9 -use "ax_ops/thy_axioms.ML";
    1.10 -use "ax_ops/thy_ops.ML";
    1.11 -use "ax_ops/thy_syntax.ML";
    1.12 +use "HOLCFLogic";
    1.13 +use "contconsts";
    1.14  
    1.15 -(* sections domain, generated *)
    1.16 -
    1.17 +(* domain package *)
    1.18  use "domain/library.ML";
    1.19  use "domain/syntax.ML";
    1.20  use "domain/axioms.ML";