# HG changeset patch
# User nipkow
# Date 1235159449 -3600
# Node ID ab40c5e007e001d114c64e27a2649ee953ec3170
# Parent  d8b6542e643f2f0160620860ead211fa0ae22c64
removed subsumed lemmas

diff -r d8b6542e643f -r ab40c5e007e0 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Feb 20 16:48:17 2009 +0100
+++ b/src/HOL/Divides.thy	Fri Feb 20 20:50:49 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 d8b6542e643f -r ab40c5e007e0 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Fri Feb 20 16:48:17 2009 +0100
+++ b/src/HOL/Groebner_Basis.thy	Fri Feb 20 20:50:49 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 d8b6542e643f -r ab40c5e007e0 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Fri Feb 20 16:48:17 2009 +0100
+++ b/src/HOL/Presburger.thy	Fri Feb 20 20:50:49 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]