# HG changeset patch
# User haftmann
# Date 1235161774 -3600
# Node ID 00d04a562df1a3784716263cdf2e9eaa6a9105e5
# Parent  f2421131a83cc39cd16ef13326eafc37dd387a87# Parent  d14d0b4bf5b466c46491e7ea0a5b341fcaed6e75
merged

diff -r d14d0b4bf5b4 -r 00d04a562df1 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Feb 20 21:29:24 2009 +0100
+++ b/src/HOL/Divides.thy	Fri Feb 20 21:29:34 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 d14d0b4bf5b4 -r 00d04a562df1 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Fri Feb 20 21:29:24 2009 +0100
+++ b/src/HOL/Groebner_Basis.thy	Fri Feb 20 21:29:34 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 d14d0b4bf5b4 -r 00d04a562df1 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Fri Feb 20 21:29:24 2009 +0100
+++ b/src/HOL/Presburger.thy	Fri Feb 20 21:29:34 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]