equal
deleted
inserted
replaced
143 fun export probfile (((proof, _), _), _) = |
143 fun export probfile (((proof, _), _), _) = |
144 if destdir' = "" then |
144 if destdir' = "" then |
145 () |
145 () |
146 else |
146 else |
147 File.write (Path.explode (Path.implode probfile ^ "_proof")) |
147 File.write (Path.explode (Path.implode probfile ^ "_proof")) |
148 ("% " ^ timestamp () ^ "\n" ^ proof) |
148 ((if overlord then |
|
149 "% " ^ cmd_line probfile ^ "\n% " ^ timestamp () ^ "\n" |
|
150 else |
|
151 "") ^ proof) |
149 |
152 |
150 val (((proof, atp_run_time_in_msecs), rc), _) = |
153 val (((proof, atp_run_time_in_msecs), rc), _) = |
151 with_path cleanup export run_on (prob_pathname subgoal); |
154 with_path cleanup export run_on (prob_pathname subgoal); |
152 |
155 |
153 (* Check for success and print out some information on failure. *) |
156 (* Check for success and print out some information on failure. *) |