src/Pure/ROOT.ML
changeset 28288 09c812966e7f
parent 28200 5ef2c4bde4e5
child 28318 6b8d001ce1de
equal deleted inserted replaced
28287:c86fa4e0aedb 28288:09c812966e7f
    59 use "pattern.ML";
    59 use "pattern.ML";
    60 use "unify.ML";
    60 use "unify.ML";
    61 use "theory.ML";
    61 use "theory.ML";
    62 use "interpretation.ML";
    62 use "interpretation.ML";
    63 use "proofterm.ML";
    63 use "proofterm.ML";
       
    64 use "deriv.ML";
    64 use "thm.ML";
    65 use "thm.ML";
    65 use "more_thm.ML";
    66 use "more_thm.ML";
    66 use "facts.ML";
    67 use "facts.ML";
    67 use "pure_thy.ML";
    68 use "pure_thy.ML";
    68 use "display.ML";
    69 use "display.ML";