src/Pure/ROOT.ML
changeset 18934 0342b7c21388
parent 18870 020e242c02a0
child 18991 0ded3b842878
equal deleted inserted replaced
18933:057b32b8f1fd 18934:0342b7c21388
    29 
    29 
    30 (*inner syntax module*)
    30 (*inner syntax module*)
    31 cd "Syntax"; use "ROOT.ML"; cd "..";
    31 cd "Syntax"; use "ROOT.ML"; cd "..";
    32 
    32 
    33 (*core of tactical proof system*)
    33 (*core of tactical proof system*)
       
    34 use "envir.ML";
       
    35 use "logic.ML";
    34 use "type_infer.ML";
    36 use "type_infer.ML";
    35 use "consts.ML";
    37 use "consts.ML";
    36 use "sign.ML";
    38 use "sign.ML";
    37 use "envir.ML";
       
    38 use "pattern.ML";
    39 use "pattern.ML";
    39 use "unify.ML";
    40 use "unify.ML";
    40 use "net.ML";
    41 use "net.ML";
    41 use "logic.ML";
       
    42 use "defs.ML";
    42 use "defs.ML";
    43 use "theory.ML";
    43 use "theory.ML";
    44 use "proofterm.ML";
    44 use "proofterm.ML";
    45 use "thm.ML";
    45 use "thm.ML";
    46 use "display.ML";
    46 use "display.ML";