src/Pure/Isar/ROOT.ML
changeset 26609 53754d9ee31f
parent 26598 1249f49d0819
child 27254 0f8106808e66
equal deleted inserted replaced
26608:ff838a61dad6 26609:53754d9ee31f
    25 use "../Thy/thy_header.ML";
    25 use "../Thy/thy_header.ML";
    26 use "../Thy/thy_load.ML";
    26 use "../Thy/thy_load.ML";
    27 use "../Thy/html.ML";
    27 use "../Thy/html.ML";
    28 use "../Thy/latex.ML";
    28 use "../Thy/latex.ML";
    29 use "../Thy/present.ML";
    29 use "../Thy/present.ML";
    30 use "../Thy/thy_info.ML";
       
    31 use "../Thy/thm_deps.ML";
       
    32 
    30 
    33 (*basic proof engine*)
    31 (*basic proof engine*)
    34 use "proof_display.ML";
    32 use "proof_display.ML";
    35 use "attrib.ML";
    33 use "attrib.ML";
    36 use "context_rules.ML";
    34 use "context_rules.ML";
    60 use "spec_parse.ML";
    58 use "spec_parse.ML";
    61 use "specification.ML";
    59 use "specification.ML";
    62 use "instance.ML";
    60 use "instance.ML";
    63 use "constdefs.ML";
    61 use "constdefs.ML";
    64 
    62 
    65 (*toplevel environment*)
    63 (*toplevel transactions*)
    66 use "proof_history.ML";
    64 use "proof_history.ML";
    67 use "toplevel.ML";
    65 use "toplevel.ML";
    68 
    66 
    69 (*theory presentation*)
    67 (*theory syntax*)
    70 use "../Thy/term_style.ML";
    68 use "../Thy/term_style.ML";
    71 use "../Thy/thy_output.ML";
    69 use "../Thy/thy_output.ML";
    72 
       
    73 (*theory syntax*)
       
    74 use "session.ML";
       
    75 use "../old_goals.ML";
    70 use "../old_goals.ML";
    76 use "outer_syntax.ML";
    71 use "outer_syntax.ML";
       
    72 use "../Thy/thy_info.ML";
       
    73 use "session.ML";
    77 use "isar.ML";
    74 use "isar.ML";
    78 use "../Thy/thy_edit.ML";
    75 use "../Thy/thy_edit.ML";
    79 
    76 
    80 (*theory and proof operations*)
    77 (*theory and proof operations*)
    81 use "rule_insts.ML";
    78 use "rule_insts.ML";
    82 use "../simplifier.ML";
    79 use "../simplifier.ML";
       
    80 use "../Thy/thm_deps.ML";
    83 use "find_theorems.ML";
    81 use "find_theorems.ML";
    84 use "isar_cmd.ML";
    82 use "isar_cmd.ML";
    85 use "isar_syn.ML";
    83 use "isar_syn.ML";