equal
deleted
inserted
replaced
167 handle TYPE _ => @{prop True} |
167 handle TYPE _ => @{prop True} |
168 end |
168 end |
169 |
169 |
170 fun generate_tptp_inference_file_for_theory ctxt thy format type_enc file_name = |
170 fun generate_tptp_inference_file_for_theory ctxt thy format type_enc file_name = |
171 let |
171 let |
172 val type_enc = type_enc |> type_enc_from_string Sound |
172 val type_enc = type_enc |> type_enc_from_string Strict |
173 |> adjust_type_enc format |
173 |> adjust_type_enc format |
174 val mono = polymorphism_of_type_enc type_enc <> Polymorphic |
174 val mono = polymorphism_of_type_enc type_enc <> Polymorphic |
175 val path = file_name |> Path.explode |
175 val path = file_name |> Path.explode |
176 val _ = File.write path "" |
176 val _ = File.write path "" |
177 val facts = facts_of thy |
177 val facts = facts_of thy |