src/Pure/ROOT.ML
changeset 38978 4bf80c23320e
parent 38874 4a4d34d2f97b
child 39214 49fc6c842d6c
equal deleted inserted replaced
38977:e71e2c56479c 38978:4bf80c23320e
   236 (*theory documents*)
   236 (*theory documents*)
   237 use "Thy/present.ML";
   237 use "Thy/present.ML";
   238 use "Thy/term_style.ML";
   238 use "Thy/term_style.ML";
   239 use "Thy/thy_output.ML";
   239 use "Thy/thy_output.ML";
   240 use "Thy/thy_syntax.ML";
   240 use "Thy/thy_syntax.ML";
   241 use "old_goals.ML";
       
   242 use "Isar/outer_syntax.ML";
   241 use "Isar/outer_syntax.ML";
   243 use "PIDE/document.ML";
   242 use "PIDE/document.ML";
   244 use "Thy/thy_info.ML";
   243 use "Thy/thy_info.ML";
   245 
   244 
   246 (*theory and proof operations*)
   245 (*theory and proof operations*)