src/Pure/ROOT.ML
changeset 27546 726e8fa3e404
parent 27262 5a5d7f55ec19
child 27642 c0db1220b071
equal deleted inserted replaced
27545:7165068bb61f 27546:726e8fa3e404
    49 
    49 
    50 (*core of tactical proof system*)
    50 (*core of tactical proof system*)
    51 use "envir.ML";
    51 use "envir.ML";
    52 use "consts.ML";
    52 use "consts.ML";
    53 use "primitive_defs.ML";
    53 use "primitive_defs.ML";
       
    54 use "defs.ML";
       
    55 use "net.ML";
    54 use "sign.ML";
    56 use "sign.ML";
    55 use "pattern.ML";
    57 use "pattern.ML";
    56 use "unify.ML";
    58 use "unify.ML";
    57 use "net.ML";
       
    58 use "defs.ML";
       
    59 use "theory.ML";
    59 use "theory.ML";
    60 use "interpretation.ML";
    60 use "interpretation.ML";
    61 use "proofterm.ML";
    61 use "proofterm.ML";
    62 use "thm.ML";
    62 use "thm.ML";
    63 use "more_thm.ML";
    63 use "more_thm.ML";