equal
deleted
inserted
replaced
62 |
62 |
63 fun has_thys thys th = exists (has_thm_thy th) thys |
63 fun has_thys thys th = exists (has_thm_thy th) thys |
64 |
64 |
65 fun all_facts ctxt = |
65 fun all_facts ctxt = |
66 let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in |
66 let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in |
67 Sledgehammer_Fact.all_facts ctxt true false Keyword.empty_keywords [] [] css |
67 Sledgehammer_Fact.all_facts ctxt true Keyword.empty_keywords [] [] css |
68 |> sort (crude_thm_ord ctxt o apply2 snd) |
68 |> sort (crude_thm_ord ctxt o apply2 snd) |
69 end |
69 end |
70 |
70 |
71 fun filter_accessible_from th = filter (fn (_, th') => thm_less (th', th)) |
71 fun filter_accessible_from th = filter (fn (_, th') => thm_less (th', th)) |
72 |
72 |
170 |
170 |
171 fun is_bad_query ctxt ho_atp step j th isar_deps = |
171 fun is_bad_query ctxt ho_atp step j th isar_deps = |
172 j mod step <> 0 orelse |
172 j mod step <> 0 orelse |
173 Thm.legacy_get_kind th = "" orelse |
173 Thm.legacy_get_kind th = "" orelse |
174 null (the_list isar_deps) orelse |
174 null (the_list isar_deps) orelse |
175 is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th) |
175 is_blacklisted_or_something (Thm.get_name_hint th) |
176 |
176 |
177 fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys max_suggs file_name = |
177 fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys max_suggs file_name = |
178 let |
178 let |
179 val ho_atp = is_ho_atp ctxt prover |
179 val ho_atp = is_ho_atp ctxt prover |
180 val path = Path.explode file_name |
180 val path = Path.explode file_name |