src/HOLCF/ROOT.ML
changeset 4041 4df7f385fe9f
parent 4010 59cac65fb751
child 4122 f63c283cefaf
equal deleted inserted replaced
4040:20f7471eedbf 4041:4df7f385fe9f
    13 print_depth 1;
    13 print_depth 1;
    14 
    14 
    15 use_thy "HOLCF";
    15 use_thy "HOLCF";
    16 
    16 
    17 (* sections axioms, ops *)
    17 (* sections axioms, ops *)
    18 
       
    19 use "ax_ops/holcflogic.ML";
    18 use "ax_ops/holcflogic.ML";
    20 use "ax_ops/thy_axioms.ML";
    19 use "ax_ops/thy_axioms.ML";
    21 use "ax_ops/thy_ops.ML";
    20 use "ax_ops/thy_ops.ML";
    22 use "ax_ops/thy_syntax.ML";
    21 use "ax_ops/thy_syntax.ML";
    23 
    22