--- a/src/HOL/Divides.thy Fri Feb 20 18:33:38 2009 +0100
+++ b/src/HOL/Divides.thy Fri Feb 20 20:51:06 2009 +0100
@@ -795,12 +795,6 @@
apply (auto simp add: Suc_diff_le le_mod_geq)
done
-lemma nat_mod_div_trivial: "m mod n div n = (0 :: nat)"
-by simp
-
-lemma nat_mod_mod_trivial: "m mod n mod n = (m mod n :: nat)"
-by simp
-
subsubsection {* The Divides Relation *}
--- a/src/HOL/Groebner_Basis.thy Fri Feb 20 18:33:38 2009 +0100
+++ b/src/HOL/Groebner_Basis.thy Fri Feb 20 20:51:06 2009 +0100
@@ -436,8 +436,8 @@
*} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
declare dvd_def[algebra]
declare dvd_eq_mod_eq_0[symmetric, algebra]
-declare nat_mod_div_trivial[algebra]
-declare nat_mod_mod_trivial[algebra]
+declare mod_div_trivial[algebra]
+declare mod_mod_trivial[algebra]
declare conjunct1[OF DIVISION_BY_ZERO, algebra]
declare conjunct2[OF DIVISION_BY_ZERO, algebra]
declare zmod_zdiv_equality[symmetric,algebra]
--- a/src/HOL/Presburger.thy Fri Feb 20 18:33:38 2009 +0100
+++ b/src/HOL/Presburger.thy Fri Feb 20 20:51:06 2009 +0100
@@ -424,7 +424,7 @@
declare zmod_self[presburger]
declare mod_self[presburger]
declare mod_by_0[presburger]
-declare nat_mod_div_trivial[presburger]
+declare mod_div_trivial[presburger]
declare div_mod_equality2[presburger]
declare div_mod_equality[presburger]
declare mod_div_equality2[presburger]