equal
deleted
inserted
replaced
240 cat_lines (map (Syntax.string_of_term ctxt o snd) props)) |
240 cat_lines (map (Syntax.string_of_term ctxt o snd) props)) |
241 *) |
241 *) |
242 val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans |
242 val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans |
243 val (atp_problem, _, _, lifted, sym_tab) = |
243 val (atp_problem, _, _, lifted, sym_tab) = |
244 prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lam_trans |
244 prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lam_trans |
245 false false [] @{prop False} props |
245 false false false [] @{prop False} props |
246 (* |
246 (* |
247 val _ = tracing ("ATP PROBLEM: " ^ |
247 val _ = tracing ("ATP PROBLEM: " ^ |
248 cat_lines (lines_for_atp_problem CNF atp_problem)) |
248 cat_lines (lines_for_atp_problem CNF atp_problem)) |
249 *) |
249 *) |
250 (* "rev" is for compatibility with existing proof scripts. *) |
250 (* "rev" is for compatibility with existing proof scripts. *) |