src/Pure/Isar/ROOT.ML
changeset 7728 2e737ce3cdb5
parent 7680 27bbbe36d49a
child 8091 226dcdc3c5f3
equal deleted inserted replaced
7727:b52c7d773121 7728:2e737ce3cdb5
    21 use "skip_proof.ML";
    21 use "skip_proof.ML";
    22 use "obtain.ML";
    22 use "obtain.ML";
    23 
    23 
    24 (*outer syntax*)
    24 (*outer syntax*)
    25 use "comment.ML";
    25 use "comment.ML";
    26 use "outer_lex.ML";
    26 (*use "outer_lex.ML";*)	  (*see ../Thy/ROOT.ML*)
    27 use "outer_parse.ML";
    27 use "outer_parse.ML";
    28 
    28 
    29 (*toplevel environment*)
    29 (*toplevel environment*)
    30 use "toplevel.ML";
    30 use "toplevel.ML";
    31 use "session.ML";
    31 use "session.ML";