equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 signature NORMALIZER = |
7 signature NORMALIZER = |
8 sig |
8 sig |
9 type entry |
9 type entry |
10 val get: Proof.context -> simpset * (thm * entry) list |
10 val get: Proof.context -> (thm * entry) list |
11 val match: Proof.context -> cterm -> entry option |
11 val match: Proof.context -> cterm -> entry option |
12 val del: attribute |
12 val del: attribute |
13 val add: {semiring: cterm list * thm list, ring: cterm list * thm list, field: cterm list * thm list, idom: thm list, ideal: thm list} |
13 val add: {semiring: cterm list * thm list, ring: cterm list * thm list, field: cterm list * thm list, idom: thm list, ideal: thm list} |
14 -> attribute |
14 -> attribute |
15 val funs: thm -> {is_const: morphism -> cterm -> bool, |
15 val funs: thm -> {is_const: morphism -> cterm -> bool, |
60 val extend = I; |
60 val extend = I; |
61 fun merge ((ss, e), (ss', e')) : T = |
61 fun merge ((ss, e), (ss', e')) : T = |
62 (merge_ss (ss, ss'), AList.merge eq_key (K true) (e, e')); |
62 (merge_ss (ss, ss'), AList.merge eq_key (K true) (e, e')); |
63 ); |
63 ); |
64 |
64 |
65 val get = Data.get o Context.Proof; |
65 val get = snd o Data.get o Context.Proof; |
66 |
66 |
67 |
67 |
68 (* match data *) |
68 (* match data *) |
69 |
69 |
70 fun match ctxt tm = |
70 fun match ctxt tm = |