equal
deleted
inserted
replaced
37 val relevance_fudge = |
37 val relevance_fudge = |
38 Sledgehammer_Provers.relevance_fudge_for_prover ctxt name |
38 Sledgehammer_Provers.relevance_fudge_for_prover ctxt name |
39 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i |
39 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i |
40 val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers |
40 val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers |
41 val facts = |
41 val facts = |
42 Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override |
42 Sledgehammer_Fact.nearly_all_facts ctxt ho_atp relevance_override |
43 chained_ths hyp_ts concl_t |
43 chained_ths hyp_ts concl_t |
44 |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds |
44 |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds |
45 (the_default default_max_relevant max_relevant) is_built_in_const |
45 (the_default default_max_relevant max_relevant) is_built_in_const |
46 relevance_fudge relevance_override chained_ths hyp_ts concl_t |
46 relevance_fudge relevance_override chained_ths hyp_ts concl_t |
47 val problem = |
47 val problem = |
48 {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, |
48 {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, |