author | desharna |
Wed, 18 Dec 2024 16:32:49 +0100 | |
changeset 81624 | 6e09005f6ca8 |
parent 81623 | a2e68976251f |
child 81625 | dee16531eaf0 |
--- 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