src/Pure/ROOT.ML
changeset 52865 02a7e7180ee5
parent 52836 1a03ffc00a4a
child 52926 6415d95bf7a2
equal deleted inserted replaced
52864:c2da0d3b974d 52865:02a7e7180ee5
   267 use "Isar/outer_syntax.ML";
   267 use "Isar/outer_syntax.ML";
   268 use "General/graph_display.ML";
   268 use "General/graph_display.ML";
   269 use "Thy/present.ML";
   269 use "Thy/present.ML";
   270 use "PIDE/execution.ML";
   270 use "PIDE/execution.ML";
   271 use "PIDE/command.ML";
   271 use "PIDE/command.ML";
       
   272 use "PIDE/query_operation.ML";
   272 use "Thy/thy_load.ML";
   273 use "Thy/thy_load.ML";
   273 use "Thy/thy_info.ML";
   274 use "Thy/thy_info.ML";
   274 use "PIDE/document.ML";
   275 use "PIDE/document.ML";
   275 use "Thy/rail.ML";
   276 use "Thy/rail.ML";
   276 
   277