equal
deleted
inserted
replaced
26 end; |
26 end; |
27 |
27 |
28 structure MaSh_Export : MASH_EXPORT = |
28 structure MaSh_Export : MASH_EXPORT = |
29 struct |
29 struct |
30 |
30 |
31 open Sledgehammer_Fact |
|
32 open Sledgehammer_MePo |
31 open Sledgehammer_MePo |
33 open Sledgehammer_MaSh |
32 open Sledgehammer_MaSh |
34 |
33 |
35 fun thy_map_from_facts ths = |
34 fun thy_map_from_facts ths = |
36 ths |> sort (thm_ord o swap o pairself snd) |
35 ths |> sort (thm_ord o swap o pairself snd) |
43 |
42 |
44 fun has_thys thys th = exists (has_thm_thy th) thys |
43 fun has_thys thys th = exists (has_thm_thy th) thys |
45 |
44 |
46 fun all_facts ctxt = |
45 fun all_facts ctxt = |
47 let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in |
46 let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in |
48 nearly_all_facts ctxt false no_fact_override Symtab.empty css [] [] |
47 Sledgehammer_Fact.all_facts ctxt false Symtab.empty [] [] css |
49 @{prop True} |
|
50 end |
48 end |
51 |
49 |
52 fun add_thy_parent_facts thy_map thy = |
50 fun add_thy_parent_facts thy_map thy = |
53 let |
51 let |
54 fun add_last thy = |
52 fun add_last thy = |