equal
deleted
inserted
replaced
168 Keyword.empty_keywords [] [] css_table |
168 Keyword.empty_keywords [] [] css_table |
169 |> sort (Sledgehammer_MaSh.crude_thm_ord o apply2 snd) |
169 |> sort (Sledgehammer_MaSh.crude_thm_ord o apply2 snd) |
170 val problem = |
170 val problem = |
171 facts |
171 facts |
172 |> map (fn ((_, loc), th) => |
172 |> map (fn ((_, loc), th) => |
173 ((Thm.get_name_hint th, loc), th |> prop_of |> mono ? monomorphize_term ctxt)) |
173 ((Thm.get_name_hint th, loc), th |> Thm.prop_of |> mono ? monomorphize_term ctxt)) |
174 |> generate_atp_problem ctxt format Axiom type_enc Exporter combsN false false true [] |
174 |> generate_atp_problem ctxt format Axiom type_enc Exporter combsN false false true [] |
175 @{prop False} |
175 @{prop False} |
176 |> #1 |> sort_wrt (heading_sort_key o fst) |
176 |> #1 |> sort_wrt (heading_sort_key o fst) |
177 val prelude = fst (split_last problem) |
177 val prelude = fst (split_last problem) |
178 val name_tabs = Sledgehammer_Fact.build_name_tables Thm.get_name_hint facts |
178 val name_tabs = Sledgehammer_Fact.build_name_tables Thm.get_name_hint facts |