equal
deleted
inserted
replaced
55 structure Data = Generic_Data |
55 structure Data = Generic_Data |
56 ( |
56 ( |
57 type T = (thm * entry) list; |
57 type T = (thm * entry) list; |
58 val empty = []; |
58 val empty = []; |
59 val extend = I; |
59 val extend = I; |
60 val merge = AList.merge Thm.eq_thm (K true); |
60 fun merge data = AList.merge Thm.eq_thm (K true) data; |
61 ); |
61 ); |
62 |
62 |
63 val get = Data.get o Context.Proof; |
63 val get = Data.get o Context.Proof; |
64 |
64 |
65 fun match ctxt tm = |
65 fun match ctxt tm = |