equal
deleted
inserted
replaced
46 fun has_thys thys th = exists (has_thm_thy th) thys |
46 fun has_thys thys th = exists (has_thm_thy th) thys |
47 |
47 |
48 fun all_facts ctxt = |
48 fun all_facts ctxt = |
49 let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in |
49 let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in |
50 Sledgehammer_Fact.all_facts ctxt true false Symtab.empty [] [] css |
50 Sledgehammer_Fact.all_facts ctxt true false Symtab.empty [] [] css |
51 |> sort (thm_ord o pairself snd) |
51 |> sort (crude_thm_ord o pairself snd) |
52 end |
52 end |
53 |
53 |
54 fun generate_accessibility ctxt thys include_thys file_name = |
54 fun generate_accessibility ctxt thys include_thys file_name = |
55 let |
55 let |
56 val path = file_name |> Path.explode |
56 val path = file_name |> Path.explode |