src/Pure/ROOT.ML
changeset 2960 a6b56d03ed0d
parent 2582 b6e37441acb8
child 3280 87e734c72152
equal deleted inserted replaced
2959:071bfb16586f 2960:a6b56d03ed0d
    23 (*Syntax module*)
    23 (*Syntax module*)
    24 cd "Syntax";
    24 cd "Syntax";
    25 use "ROOT.ML";
    25 use "ROOT.ML";
    26 cd "..";
    26 cd "..";
    27 
    27 
       
    28 use "sorts.ML";
       
    29 use "type_infer.ML";
    28 use "type.ML";
    30 use "type.ML";
    29 use "sign.ML";
    31 use "sign.ML";
    30 use "sequence.ML";
    32 use "sequence.ML";
    31 use "envir.ML";
    33 use "envir.ML";
    32 use "pattern.ML";
    34 use "pattern.ML";