equal
deleted
inserted
replaced
158 val facts = facts_of thy |
158 val facts = facts_of thy |
159 val (atp_problem, _, _, _, _, _, _) = |
159 val (atp_problem, _, _, _, _, _, _) = |
160 facts |
160 facts |
161 |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th)) |
161 |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th)) |
162 |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true |
162 |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true |
163 combinatorsN false true [] @{prop False} |
163 (map (introduce_combinators ctxt)) false true [] |
|
164 @{prop False} |
164 val atp_problem = |
165 val atp_problem = |
165 atp_problem |
166 atp_problem |
166 |> map (apsnd (filter_out (is_problem_line_tautology ctxt))) |
167 |> map (apsnd (filter_out (is_problem_line_tautology ctxt))) |
167 val all_names = facts |> map (Thm.get_name_hint o snd) |
168 val all_names = facts |> map (Thm.get_name_hint o snd) |
168 val infers = |
169 val infers = |