removed subsumed lemmas
authornipkow
Fri Feb 20 20:50:49 2009 +0100 (2009-02-20)
changeset 30027ab40c5e007e0
parent 30017 d8b6542e643f
child 30028 f2421131a83c
removed subsumed lemmas
src/HOL/Divides.thy
src/HOL/Groebner_Basis.thy
src/HOL/Presburger.thy
     1.1 --- a/src/HOL/Divides.thy	Fri Feb 20 16:48:17 2009 +0100
     1.2 +++ b/src/HOL/Divides.thy	Fri Feb 20 20:50:49 2009 +0100
     1.3 @@ -795,12 +795,6 @@
     1.4  apply (auto simp add: Suc_diff_le le_mod_geq)
     1.5  done
     1.6  
     1.7 -lemma nat_mod_div_trivial: "m mod n div n = (0 :: nat)"
     1.8 -by simp
     1.9 -
    1.10 -lemma nat_mod_mod_trivial: "m mod n mod n = (m mod n :: nat)"
    1.11 -by simp
    1.12 -
    1.13  
    1.14  subsubsection {* The Divides Relation *}
    1.15  
     2.1 --- a/src/HOL/Groebner_Basis.thy	Fri Feb 20 16:48:17 2009 +0100
     2.2 +++ b/src/HOL/Groebner_Basis.thy	Fri Feb 20 20:50:49 2009 +0100
     2.3 @@ -436,8 +436,8 @@
     2.4  *} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
     2.5  declare dvd_def[algebra]
     2.6  declare dvd_eq_mod_eq_0[symmetric, algebra]
     2.7 -declare nat_mod_div_trivial[algebra]
     2.8 -declare nat_mod_mod_trivial[algebra]
     2.9 +declare mod_div_trivial[algebra]
    2.10 +declare mod_mod_trivial[algebra]
    2.11  declare conjunct1[OF DIVISION_BY_ZERO, algebra]
    2.12  declare conjunct2[OF DIVISION_BY_ZERO, algebra]
    2.13  declare zmod_zdiv_equality[symmetric,algebra]
     3.1 --- a/src/HOL/Presburger.thy	Fri Feb 20 16:48:17 2009 +0100
     3.2 +++ b/src/HOL/Presburger.thy	Fri Feb 20 20:50:49 2009 +0100
     3.3 @@ -424,7 +424,7 @@
     3.4  declare zmod_self[presburger]
     3.5  declare mod_self[presburger]
     3.6  declare mod_by_0[presburger]
     3.7 -declare nat_mod_div_trivial[presburger]
     3.8 +declare mod_div_trivial[presburger]
     3.9  declare div_mod_equality2[presburger]
    3.10  declare div_mod_equality[presburger]
    3.11  declare mod_div_equality2[presburger]