changeset 81624 | 6e09005f6ca8 |
parent 78788 | 5a14f2cc1ea0 |
child 82135 | 08475a3360a8 |
--- a/src/HOL/Tools/ATP/atp_problem.ML Wed Dec 18 16:20:34 2024 +0100 +++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Dec 18 16:32:49 2024 +0100 @@ -801,8 +801,8 @@ end fun lines_of_atp_problem format ord_info problem = - "% This file was generated by Isabelle (most likely Sledgehammer)\n\ - \% " ^ timestamp () ^ "\n" :: + "% This file was generated by Isabelle (most likely Sledgehammer)" :: + timestamp () :: (case format of DFG poly => dfg_lines poly ord_info | _ => tptp_lines format) problem