src/HOL/ex/atp_export.ML
changeset 43224 97906dfd39b7
parent 43223 c9e87dc92d9e
child 43245 cef69d31bfa4
equal deleted inserted replaced
43223:c9e87dc92d9e 43224:97906dfd39b7
   112                         (fact_name_of (Thm.get_name_hint th),
   112                         (fact_name_of (Thm.get_name_hint th),
   113                          theorems_mentioned_in_proof_term th))
   113                          theorems_mentioned_in_proof_term th))
   114     val infers =
   114     val infers =
   115       infers |> map (apsnd (filter (member (op = o apsnd fst) infers)))
   115       infers |> map (apsnd (filter (member (op = o apsnd fst) infers)))
   116     val atp_problem = atp_problem |> add_inferences_to_problem infers
   116     val atp_problem = atp_problem |> add_inferences_to_problem infers
   117     val ss =
   117     val ss = ATP_Problem.tptp_lines_for_atp_problem ATP_Problem.FOF atp_problem
   118       ATP_Problem.tptp_strings_for_atp_problem ATP_Problem.FOF atp_problem
       
   119     val _ = app (File.append path) ss
   118     val _ = app (File.append path) ss
   120   in () end
   119   in () end
   121 
   120 
   122 end;
   121 end;