src/HOL/Groebner_Basis.thy
changeset 58777 6ba2f1fa243b
parent 57951 7896762b638b
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Groebner_Basis.thy	Fri Oct 24 15:07:51 2014 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Thu Oct 23 19:40:39 2014 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Groebner bases *}
     1.5  
     1.6  theory Groebner_Basis
     1.7 -imports Semiring_Normalization
     1.8 +imports Semiring_Normalization Parity
     1.9  keywords "try0" :: diag
    1.10  begin
    1.11  
    1.12 @@ -77,4 +77,22 @@
    1.13  declare zmod_eq_dvd_iff[algebra]
    1.14  declare nat_mod_eq_iff[algebra]
    1.15  
    1.16 +context semiring_parity
    1.17 +begin
    1.18 +
    1.19 +declare even_times_iff [algebra]
    1.20 +declare even_power [algebra]
    1.21 +
    1.22  end
    1.23 +
    1.24 +context ring_parity
    1.25 +begin
    1.26 +
    1.27 +declare even_minus [algebra]
    1.28 +
    1.29 +end
    1.30 +
    1.31 +declare even_Suc [algebra]
    1.32 +declare even_diff_nat [algebra]
    1.33 +
    1.34 +end