16 val declare: thm -> {semiring: term list * thm list, ring: term list * thm list, |
16 val declare: thm -> {semiring: term list * thm list, ring: term list * thm list, |
17 field: term list * thm list, idom: thm list, ideal: thm list} -> |
17 field: term list * thm list, idom: thm list, ideal: thm list} -> |
18 local_theory -> local_theory |
18 local_theory -> local_theory |
19 |
19 |
20 val semiring_normalize_conv: Proof.context -> conv |
20 val semiring_normalize_conv: Proof.context -> conv |
21 val semiring_normalize_ord_conv: Proof.context -> (cterm * cterm -> order) -> conv |
21 val semiring_normalize_ord_conv: Proof.context -> cterm ord -> conv |
22 val semiring_normalize_wrapper: Proof.context -> entry -> conv |
22 val semiring_normalize_wrapper: Proof.context -> entry -> conv |
23 val semiring_normalize_ord_wrapper: Proof.context -> entry |
23 val semiring_normalize_ord_wrapper: Proof.context -> entry -> cterm ord -> conv |
24 -> (cterm * cterm -> order) -> conv |
|
25 val semiring_normalizers_conv: cterm list -> cterm list * thm list |
24 val semiring_normalizers_conv: cterm list -> cterm list * thm list |
26 -> cterm list * thm list -> cterm list * thm list -> |
25 -> cterm list * thm list -> cterm list * thm list -> |
27 (cterm -> bool) * conv * conv * conv -> (cterm * cterm -> order) -> |
26 (cterm -> bool) * conv * conv * conv -> cterm ord -> |
28 {add: Proof.context -> conv, |
27 {add: Proof.context -> conv, |
29 mul: Proof.context -> conv, |
28 mul: Proof.context -> conv, |
30 neg: Proof.context -> conv, |
29 neg: Proof.context -> conv, |
31 main: Proof.context -> conv, |
30 main: Proof.context -> conv, |
32 pow: Proof.context -> conv, |
31 pow: Proof.context -> conv, |
33 sub: Proof.context -> conv} |
32 sub: Proof.context -> conv} |
34 val semiring_normalizers_ord_wrapper: Proof.context -> entry -> |
33 val semiring_normalizers_ord_wrapper: Proof.context -> entry -> cterm ord -> |
35 (cterm * cterm -> order) -> |
|
36 {add: Proof.context -> conv, |
34 {add: Proof.context -> conv, |
37 mul: Proof.context -> conv, |
35 mul: Proof.context -> conv, |
38 neg: Proof.context -> conv, |
36 neg: Proof.context -> conv, |
39 main: Proof.context -> conv, |
37 main: Proof.context -> conv, |
40 pow: Proof.context -> conv, |
38 pow: Proof.context -> conv, |