src/Pure/ROOT.ML
changeset 15006 107e4dfd3b96
parent 14823 ebb8499d0fd2
child 15481 fc075ae929e4
equal deleted inserted replaced
15005:546c8e7e28d4 15006:107e4dfd3b96
    43 use "thm.ML";
    43 use "thm.ML";
    44 use "display.ML";
    44 use "display.ML";
    45 use "fact_index.ML";
    45 use "fact_index.ML";
    46 use "pure_thy.ML";
    46 use "pure_thy.ML";
    47 use "drule.ML";
    47 use "drule.ML";
    48 use "meta_simplifier.ML";
       
    49 use "tctical.ML";
    48 use "tctical.ML";
    50 use "search.ML";
    49 use "search.ML";
       
    50 use "meta_simplifier.ML";
    51 use "tactic.ML";
    51 use "tactic.ML";
    52 
    52 
    53 (*proof term operations*)
    53 (*proof term operations*)
    54 cd "Proof"; use "ROOT.ML"; cd "..";
    54 cd "Proof"; use "ROOT.ML"; cd "..";
    55 
    55