src/Pure/ROOT.ML
changeset 4270 957c887b89b5
parent 4256 e768c42069bb
child 4278 c64867c093fb
equal deleted inserted replaced
4269:a045600f0c98 4270:957c887b89b5
    25 (*Core system*)
    25 (*Core system*)
    26 use "sorts.ML";
    26 use "sorts.ML";
    27 use "type_infer.ML";
    27 use "type_infer.ML";
    28 use "type.ML";
    28 use "type.ML";
    29 use "sign.ML";
    29 use "sign.ML";
    30 use "sequence.ML";
    30 use "seq.ML";
    31 use "envir.ML";
    31 use "envir.ML";
    32 use "pattern.ML";
    32 use "pattern.ML";
    33 use "unify.ML";
    33 use "unify.ML";
    34 use "net.ML";
    34 use "net.ML";
    35 use "logic.ML";
    35 use "logic.ML";