equal
deleted
inserted
replaced
24 val MeshN = "Mesh" |
24 val MeshN = "Mesh" |
25 val IsarN = "Isar" |
25 val IsarN = "Isar" |
26 |
26 |
27 val max_facts_slack = 2 |
27 val max_facts_slack = 2 |
28 |
28 |
29 val all_names = |
29 val all_names = map (rpair () o nickname_of) #> Symtab.make |
30 filter_out is_likely_tautology_or_too_meta |
|
31 #> map (rpair () o nickname_of) #> Symtab.make |
|
32 |
30 |
33 fun evaluate_mash_suggestions ctxt params thy file_name = |
31 fun evaluate_mash_suggestions ctxt params thy file_name = |
34 let |
32 let |
35 val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = |
33 val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = |
36 Sledgehammer_Isar.default_params ctxt [] |
34 Sledgehammer_Isar.default_params ctxt [] |