generate command-line in addition to timestamp in ATP output file, for debugging purposes
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Wed Apr 21 16:21:19 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Wed Apr 21 16:38:03 2010 +0200
@@ -145,7 +145,10 @@
()
else
File.write (Path.explode (Path.implode probfile ^ "_proof"))
- ("% " ^ timestamp () ^ "\n" ^ proof)
+ ((if overlord then
+ "% " ^ cmd_line probfile ^ "\n% " ^ timestamp () ^ "\n"
+ else
+ "") ^ proof)
val (((proof, atp_run_time_in_msecs), rc), _) =
with_path cleanup export run_on (prob_pathname subgoal);