src/Pure/ROOT.ML
changeset 3864 e0ce3d4ec47d
parent 3763 31ec17820f49
child 3971 b19d38604042
equal deleted inserted replaced
3863:7ebf561cbbb4 3864:e0ce3d4ec47d
    27 cd "..";
    27 cd "..";
    28 
    28 
    29 use "sorts.ML";
    29 use "sorts.ML";
    30 use "type_infer.ML";
    30 use "type_infer.ML";
    31 use "type.ML";
    31 use "type.ML";
       
    32 use "data.ML";
    32 use "sign.ML";
    33 use "sign.ML";
    33 use "sequence.ML";
    34 use "sequence.ML";
    34 use "envir.ML";
    35 use "envir.ML";
    35 use "pattern.ML";
    36 use "pattern.ML";
    36 use "unify.ML";
    37 use "unify.ML";