src/HOL/Library/Poly_Deriv.thy
changeset 35050 9f841f20dca6
parent 31881 eba74a5790d2
child 41959 b460124855b8
     1.1 --- a/src/HOL/Library/Poly_Deriv.thy	Mon Feb 08 17:12:32 2010 +0100
     1.2 +++ b/src/HOL/Library/Poly_Deriv.thy	Mon Feb 08 17:12:38 2010 +0100
     1.3 @@ -139,7 +139,7 @@
     1.4  lemma dvd_add_cancel1:
     1.5    fixes a b c :: "'a::comm_ring_1"
     1.6    shows "a dvd b + c \<Longrightarrow> a dvd b \<Longrightarrow> a dvd c"
     1.7 -  by (drule (1) Ring_and_Field.dvd_diff, simp)
     1.8 +  by (drule (1) Rings.dvd_diff, simp)
     1.9  
    1.10  lemma lemma_order_pderiv [rule_format]:
    1.11       "\<forall>p q a. 0 < n &