# HG changeset patch
# User nipkow
# Date 1235159466 -3600
# Node ID f2421131a83cc39cd16ef13326eafc37dd387a87
# Parent  be13af70c27c13a6beeafaa6b1d4d123f99d4076# Parent  ab40c5e007e001d114c64e27a2649ee953ec3170
merged

diff -r be13af70c27c -r f2421131a83c src/HOL/Divides.thy
--- 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 *}
 
diff -r be13af70c27c -r f2421131a83c src/HOL/Groebner_Basis.thy
--- 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]
diff -r be13af70c27c -r f2421131a83c src/HOL/Presburger.thy
--- 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]