equal
deleted
inserted
replaced
307 ML_file "PIDE/command.ML"; |
307 ML_file "PIDE/command.ML"; |
308 ML_file "PIDE/query_operation.ML"; |
308 ML_file "PIDE/query_operation.ML"; |
309 ML_file "PIDE/resources.ML"; |
309 ML_file "PIDE/resources.ML"; |
310 ML_file "Thy/present.ML"; |
310 ML_file "Thy/present.ML"; |
311 ML_file "Thy/thy_info.ML"; |
311 ML_file "Thy/thy_info.ML"; |
|
312 ML_file "Thy/thm_deps.ML"; |
312 ML_file "Thy/export_theory.ML"; |
313 ML_file "Thy/export_theory.ML"; |
313 ML_file "Thy/sessions.ML"; |
314 ML_file "Thy/sessions.ML"; |
314 ML_file "PIDE/session.ML"; |
315 ML_file "PIDE/session.ML"; |
315 ML_file "PIDE/protocol_message.ML"; |
316 ML_file "PIDE/protocol_message.ML"; |
316 ML_file "PIDE/document.ML"; |
317 ML_file "PIDE/document.ML"; |
339 ML_file "Tools/build.ML"; |
340 ML_file "Tools/build.ML"; |
340 ML_file "Tools/named_thms.ML"; |
341 ML_file "Tools/named_thms.ML"; |
341 ML_file "Tools/print_operation.ML"; |
342 ML_file "Tools/print_operation.ML"; |
342 ML_file "Tools/rail.ML"; |
343 ML_file "Tools/rail.ML"; |
343 ML_file "Tools/rule_insts.ML"; |
344 ML_file "Tools/rule_insts.ML"; |
344 ML_file "Tools/thm_deps.ML"; |
|
345 ML_file "Tools/thy_deps.ML"; |
345 ML_file "Tools/thy_deps.ML"; |
346 ML_file "Tools/class_deps.ML"; |
346 ML_file "Tools/class_deps.ML"; |
347 ML_file "Tools/find_theorems.ML"; |
347 ML_file "Tools/find_theorems.ML"; |
348 ML_file "Tools/find_consts.ML"; |
348 ML_file "Tools/find_consts.ML"; |
349 ML_file "Tools/simplifier_trace.ML"; |
349 ML_file "Tools/simplifier_trace.ML"; |