--- a/src/HOL/Decision_Procs/Ferrack.thy Wed Mar 04 10:43:39 2009 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy Wed Mar 04 10:45:52 2009 +0100
@@ -501,9 +501,9 @@
assumes gdg: "g dvd g'" and dgt':"dvdnumcoeff t g'"
shows "dvdnumcoeff t g"
using dgt' gdg
- by (induct t rule: dvdnumcoeff.induct, simp_all add: gdg zdvd_trans[OF gdg])
+ by (induct t rule: dvdnumcoeff.induct, simp_all add: gdg dvd_trans[OF gdg])
-declare zdvd_trans [trans add]
+declare dvd_trans [trans add]
lemma natabs0: "(nat (abs x) = 0) = (x = 0)"
by arith