src/HOL/Tools/ATP/atp_proof_reconstruct.ML
changeset 56854 ddd3af5a683d
parent 56254 a2dd9200854d
child 57199 472360558b22
equal deleted inserted replaced
56853:a265e41cc33b 56854:ddd3af5a683d
   494 
   494 
   495 val waldmeister_conjecture_num = "1.0.0.0"
   495 val waldmeister_conjecture_num = "1.0.0.0"
   496 
   496 
   497 fun repair_waldmeister_endgame proof =
   497 fun repair_waldmeister_endgame proof =
   498   let
   498   let
   499     fun repair_tail (name, _, t, rule, deps) = (name, Negated_Conjecture, s_not t, rule, deps)
   499     fun repair_tail (name, _, @{const Trueprop} $ t, rule, deps) =
       
   500       (name, Negated_Conjecture, @{const Trueprop} $ s_not t, rule, deps)
   500     fun repair_body [] = []
   501     fun repair_body [] = []
   501       | repair_body ((line as ((num, _), _, _, _, _)) :: lines) =
   502       | repair_body ((line as ((num, _), _, _, _, _)) :: lines) =
   502         if num = waldmeister_conjecture_num then map repair_tail (line :: lines)
   503         if num = waldmeister_conjecture_num then map repair_tail (line :: lines)
   503         else line :: repair_body lines
   504         else line :: repair_body lines
   504   in
   505   in