equal
deleted
inserted
replaced
79 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
79 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
80 val mepo_facts = |
80 val mepo_facts = |
81 Sledgehammer_MePo.mepo_suggested_facts ctxt params prover |
81 Sledgehammer_MePo.mepo_suggested_facts ctxt params prover |
82 slack_max_facts NONE hyp_ts concl_t facts |
82 slack_max_facts NONE hyp_ts concl_t facts |
83 |> Sledgehammer_MePo.weight_mepo_facts |
83 |> Sledgehammer_MePo.weight_mepo_facts |
84 val mash_facts = |
84 val (mash_facts, mash_unks) = |
85 find_mash_suggestions slack_max_facts suggs facts [] [] |
85 find_mash_suggestions slack_max_facts suggs facts [] [] |
86 |> weight_mash_facts |
86 |>> weight_mash_facts |
87 val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, []))] |
87 val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, mash_unks))] |
88 val mesh_facts = mesh_facts slack_max_facts mess |
88 val mesh_facts = mesh_facts slack_max_facts mess |
89 val isar_facts = find_suggested_facts (map (rpair 1.0) isar_deps) facts |
89 val isar_facts = find_suggested_facts (map (rpair 1.0) isar_deps) facts |
90 fun prove ok heading get facts = |
90 fun prove ok heading get facts = |
91 let |
91 let |
92 val facts = |
92 val facts = |