equal
deleted
inserted
replaced
14 val add: {semiring: cterm list * thm list, ring: cterm list * thm list, idom: thm list} |
14 val add: {semiring: cterm list * thm list, ring: cterm list * thm list, idom: thm list} |
15 -> attribute |
15 -> attribute |
16 val funs: thm -> {is_const: morphism -> cterm -> bool, |
16 val funs: thm -> {is_const: morphism -> cterm -> bool, |
17 dest_const: morphism -> cterm -> Rat.rat, |
17 dest_const: morphism -> cterm -> Rat.rat, |
18 mk_const: morphism -> ctyp -> Rat.rat -> cterm, |
18 mk_const: morphism -> ctyp -> Rat.rat -> cterm, |
19 conv: morphism -> cterm -> thm} -> morphism -> Context.generic -> Context.generic |
19 conv: morphism -> Proof.context -> cterm -> thm} -> morphism -> Context.generic -> Context.generic |
20 val setup: theory -> theory |
20 val setup: theory -> theory |
21 end; |
21 end; |
22 |
22 |
23 structure NormalizerData: NORMALIZER_DATA = |
23 structure NormalizerData: NORMALIZER_DATA = |
24 struct |
24 struct |
31 ring: cterm list * thm list, |
31 ring: cterm list * thm list, |
32 idom: thm list} * |
32 idom: thm list} * |
33 {is_const: cterm -> bool, |
33 {is_const: cterm -> bool, |
34 dest_const: cterm -> Rat.rat, |
34 dest_const: cterm -> Rat.rat, |
35 mk_const: ctyp -> Rat.rat -> cterm, |
35 mk_const: ctyp -> Rat.rat -> cterm, |
36 conv: cterm -> thm}; |
36 conv: Proof.context -> cterm -> thm}; |
37 |
37 |
38 val eq_key = Thm.eq_thm; |
38 val eq_key = Thm.eq_thm; |
39 fun eq_data arg = eq_fst eq_key arg; |
39 fun eq_data arg = eq_fst eq_key arg; |
40 |
40 |
41 structure Data = GenericDataFun |
41 structure Data = GenericDataFun |