equal
deleted
inserted
replaced
194 (* |
194 (* |
195 val _ = |
195 val _ = |
196 tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props)) |
196 tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props)) |
197 *) |
197 *) |
198 val (atp_problem, _, _, _, _, _, sym_tab) = |
198 val (atp_problem, _, _, _, _, _, sym_tab) = |
199 prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false false |
199 prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false |
200 false [] @{prop False} props |
200 combinatorsN false false [] @{prop False} props |
201 (* |
201 (* |
202 val _ = tracing ("ATP PROBLEM: " ^ |
202 val _ = tracing ("ATP PROBLEM: " ^ |
203 cat_lines (tptp_lines_for_atp_problem CNF atp_problem)) |
203 cat_lines (tptp_lines_for_atp_problem CNF atp_problem)) |
204 *) |
204 *) |
205 (* "rev" is for compatibility *) |
205 (* "rev" is for compatibility *) |