src/HOLCF/IMP/ROOT.ML
changeset 3663 e2d1e1151314
parent 2798 f84be65745b2
child 3954 c8c188655948
equal deleted inserted replaced
3662:4be700757406 3663:e2d1e1151314
    13 use_thy "Natural";
    13 use_thy "Natural";
    14 
    14 
    15 make_html := old_make_html;
    15 make_html := old_make_html;
    16 loadpath := ["."];
    16 loadpath := ["."];
    17 
    17 
    18 use_thy "Denotational";
    18 use_thy "HoareEx";