src/Pure/ROOT.ML
changeset 5244 5313f781efe0
parent 5211 c02b0c727780
child 5568 0067dd151d7a
equal deleted inserted replaced
5243:a0688fa916af 5244:5313f781efe0
    39 use "display.ML";
    39 use "display.ML";
    40 use "attribute.ML";
    40 use "attribute.ML";
    41 use "pure_thy.ML";
    41 use "pure_thy.ML";
    42 use "deriv.ML";
    42 use "deriv.ML";
    43 use "drule.ML";
    43 use "drule.ML";
       
    44 use "locale.ML";
    44 use "tctical.ML";
    45 use "tctical.ML";
    45 use "search.ML";
    46 use "search.ML";
    46 use "tactic.ML";
    47 use "tactic.ML";
    47 use "goals.ML";
    48 use "goals.ML";
    48 use "axclass.ML";
    49 use "axclass.ML";