equal
deleted
inserted
replaced
112 val goal = goal_of_thm thy th |
112 val goal = goal_of_thm thy th |
113 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
113 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
114 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
114 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
115 val isa_facts = sugg_facts hyp_ts concl_t facts isa_deps |
115 val isa_facts = sugg_facts hyp_ts concl_t facts isa_deps |
116 val iter_facts = |
116 val iter_facts = |
117 iter_facts ctxt params (max_relevant_slack * the max_relevant) goal |
117 Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params |
118 facts |
118 prover_name (max_relevant_slack * the max_relevant) NONE hyp_ts |
|
119 concl_t facts |
119 val mash_facts = sugg_facts hyp_ts concl_t facts suggs |
120 val mash_facts = sugg_facts hyp_ts concl_t facts suggs |
120 val iter_mash_facts = hybrid_facts (iter_facts, mash_facts) |
121 val iter_mash_facts = hybrid_facts (iter_facts, mash_facts) |
121 val iter_s = prove iter_ok iterN iter_facts goal |
122 val iter_s = prove iter_ok iterN iter_facts goal |
122 val mash_s = prove mash_ok mashN mash_facts goal |
123 val mash_s = prove mash_ok mashN mash_facts goal |
123 val iter_mash_s = prove iter_mash_ok iter_mashN iter_mash_facts goal |
124 val iter_mash_s = prove iter_mash_ok iter_mashN iter_mash_facts goal |