src/Pure/Isar/ROOT.ML
changeset 27613 0e03b957c649
parent 27581 db431936de07
child 27685 cd561f58076d
equal deleted inserted replaced
27612:d3eb431db035 27613:0e03b957c649
    79 use "../Thy/term_style.ML";
    79 use "../Thy/term_style.ML";
    80 use "../Thy/thy_output.ML";
    80 use "../Thy/thy_output.ML";
    81 use "../old_goals.ML";
    81 use "../old_goals.ML";
    82 use "outer_syntax.ML";
    82 use "outer_syntax.ML";
    83 use "../Thy/thy_info.ML";
    83 use "../Thy/thy_info.ML";
       
    84 use "../Thy/thy_edit.ML";
    84 use "session.ML";
    85 use "session.ML";
    85 use "isar.ML";
    86 use "isar.ML";
    86 use "../Thy/thy_edit.ML";
       
    87 
    87 
    88 (*theory and proof operations*)
    88 (*theory and proof operations*)
    89 use "rule_insts.ML";
    89 use "rule_insts.ML";
    90 use "../Thy/thm_deps.ML";
    90 use "../Thy/thm_deps.ML";
    91 use "find_theorems.ML";
    91 use "find_theorems.ML";