src/Pure/ROOT.ML
changeset 39508 dfacdb01e1ec
parent 39290 44e4d8dfd6bf
child 39557 fe5722fce758
equal deleted inserted replaced
39507:839873937ddd 39508:dfacdb01e1ec
    94 use "term_ord.ML";
    94 use "term_ord.ML";
    95 use "term_subst.ML";
    95 use "term_subst.ML";
    96 use "old_term.ML";
    96 use "old_term.ML";
    97 use "General/pretty.ML";
    97 use "General/pretty.ML";
    98 use "context.ML";
    98 use "context.ML";
       
    99 use "config.ML";
    99 use "context_position.ML";
   100 use "context_position.ML";
   100 use "sorts.ML";
   101 use "sorts.ML";
   101 use "type.ML";
   102 use "type.ML";
   102 use "logic.ML";
   103 use "logic.ML";
   103 use "Syntax/lexicon.ML";
   104 use "Syntax/lexicon.ML";
   104 use "Syntax/simple_syntax.ML";
   105 use "Syntax/simple_syntax.ML";
   105 use "config.ML";
       
   106 
   106 
   107 
   107 
   108 (* inner syntax *)
   108 (* inner syntax *)
   109 
   109 
   110 use "Syntax/ast.ML";
   110 use "Syntax/ast.ML";