39 mul: Proof.context -> conv, |
39 mul: Proof.context -> conv, |
40 neg: Proof.context -> conv, |
40 neg: Proof.context -> conv, |
41 main: Proof.context -> conv, |
41 main: Proof.context -> conv, |
42 pow: Proof.context -> conv, |
42 pow: Proof.context -> conv, |
43 sub: Proof.context -> conv} |
43 sub: Proof.context -> conv} |
44 |
|
45 val setup: theory -> theory |
|
46 end |
44 end |
47 |
45 |
48 structure Semiring_Normalizer: SEMIRING_NORMALIZER = |
46 structure Semiring_Normalizer: SEMIRING_NORMALIZER = |
49 struct |
47 struct |
50 |
48 |
910 |
908 |
911 fun optional scan = Scan.optional scan []; |
909 fun optional scan = Scan.optional scan []; |
912 |
910 |
913 in |
911 in |
914 |
912 |
915 val setup = |
913 val _ = |
916 Attrib.setup @{binding normalizer} |
914 Theory.setup |
917 (Scan.lift (Args.$$$ delN >> K del) || |
915 (Attrib.setup @{binding normalizer} |
918 ((keyword2 semiringN opsN |-- terms) -- |
916 (Scan.lift (Args.$$$ delN >> K del) || |
919 (keyword2 semiringN rulesN |-- thms)) -- |
917 ((keyword2 semiringN opsN |-- terms) -- |
920 (optional (keyword2 ringN opsN |-- terms) -- |
918 (keyword2 semiringN rulesN |-- thms)) -- |
921 optional (keyword2 ringN rulesN |-- thms)) -- |
919 (optional (keyword2 ringN opsN |-- terms) -- |
922 (optional (keyword2 fieldN opsN |-- terms) -- |
920 optional (keyword2 ringN rulesN |-- thms)) -- |
923 optional (keyword2 fieldN rulesN |-- thms)) -- |
921 (optional (keyword2 fieldN opsN |-- terms) -- |
924 optional (keyword2 idomN rulesN |-- thms) -- |
922 optional (keyword2 fieldN rulesN |-- thms)) -- |
925 optional (keyword2 idealN rulesN |-- thms) |
923 optional (keyword2 idomN rulesN |-- thms) -- |
926 >> (fn ((((sr, r), f), id), idl) => |
924 optional (keyword2 idealN rulesN |-- thms) |
927 add {semiring = sr, ring = r, field = f, idom = id, ideal = idl})) |
925 >> (fn ((((sr, r), f), id), idl) => |
928 "semiring normalizer data"; |
926 add {semiring = sr, ring = r, field = f, idom = id, ideal = idl})) |
|
927 "semiring normalizer data"); |
929 |
928 |
930 end; |
929 end; |
931 |
930 |
932 end; |
931 end; |