src/Pure/ROOT.ML
changeset 15825 1576f9d3ffae
parent 15801 d2f5ca3c048d
child 16108 cf468b93a02e
equal deleted inserted replaced
15824:222eeb9655f3 15825:1576f9d3ffae
    26 use "type.ML";
    26 use "type.ML";
    27 
    27 
    28 (*inner syntax module*)
    28 (*inner syntax module*)
    29 cd "Syntax"; use "ROOT.ML"; cd "..";
    29 cd "Syntax"; use "ROOT.ML"; cd "..";
    30 
    30 
    31 (*core system*)
    31 (*core of tactical proof system*)
    32 use "type_infer.ML";
    32 use "type_infer.ML";
    33 use "sign.ML";
    33 use "sign.ML";
    34 use "envir.ML";
    34 use "envir.ML";
    35 use "pattern.ML";
    35 use "pattern.ML";
    36 use "unify.ML";
    36 use "unify.ML";
    49 use "search.ML";
    49 use "search.ML";
    50 use "meta_simplifier.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 use "Proof/reconstruct.ML";
       
    55 use "Proof/proof_syntax.ML";
       
    56 use "Proof/proof_rewrite_rules.ML";
       
    57 use "Proof/proofchecker.ML";
    55 
    58 
    56 (*theory system operations*)
    59 (*theory auto loader database*)
    57 cd "Thy"; use "ROOT.ML"; cd "..";
    60 use "Thy/thy_load.ML";
       
    61 use "Thy/thy_info.ML";
       
    62 
       
    63 (*theory syntax -- old format*)
       
    64 use "Thy/thy_scan.ML";
       
    65 use "Thy/thy_parse.ML";
       
    66 use "Thy/thy_syn.ML";
       
    67 
       
    68 (*theory syntax -- new format*)
       
    69 use "Isar/outer_lex.ML";
       
    70 
       
    71 (*theory presentation*)
       
    72 use "Thy/html.ML";
       
    73 use "Thy/latex.ML";
       
    74 use "Thy/present.ML";
       
    75 use "Thy/thm_deps.ML";
       
    76 
       
    77 (*theorem database ML interface*)
       
    78 use "Thy/thm_database.ML";
    58 
    79 
    59 (*the Isar subsystem*)
    80 (*the Isar subsystem*)
    60 cd "Isar"; use "ROOT.ML"; cd "..";
    81 cd "Isar"; use "ROOT.ML"; cd "..";
    61 
    82 
    62 use "axclass.ML";
    83 use "axclass.ML";