equal
deleted
inserted
replaced
89 |>> weight_mash_facts |
89 |>> weight_mash_facts |
90 val mess = |
90 val mess = |
91 [(mepo_weight, (mepo_facts, [])), |
91 [(mepo_weight, (mepo_facts, [])), |
92 (mash_weight, (mash_facts, mash_unks))] |
92 (mash_weight, (mash_facts, mash_unks))] |
93 val mesh_facts = |
93 val mesh_facts = |
94 mesh_facts (Thm.eq_thm o pairself snd) slack_max_facts mess |
94 mesh_facts (Thm.eq_thm_prop o pairself snd) slack_max_facts mess |
95 val isar_facts = |
95 val isar_facts = |
96 find_suggested_facts (map (rpair 1.0) isar_deps) facts |
96 find_suggested_facts (map (rpair 1.0) isar_deps) facts |
97 (* adapted from "mirabelle_sledgehammer.ML" *) |
97 (* adapted from "mirabelle_sledgehammer.ML" *) |
98 fun set_file_name heading (SOME dir) = |
98 fun set_file_name heading (SOME dir) = |
99 let |
99 let |