--- a/src/HOL/Word/WordArith.thy Fri May 08 13:34:27 2009 +0200
+++ b/src/HOL/Word/WordArith.thy Fri May 08 13:38:21 2009 +0200
@@ -701,7 +701,8 @@
apply (erule (2) udvd_decr0)
done
-ML{*Delsimprocs cancel_factors*}
+ML {* Delsimprocs Numeral_Simprocs.cancel_factors *}
+
lemma udvd_incr2_K:
"p < a + s ==> a <= a + s ==> K udvd s ==> K udvd p - a ==> a <= p ==>
0 < K ==> p <= p + K & p + K <= a + s"
@@ -717,7 +718,8 @@
apply arith
apply simp
done
-ML{*Delsimprocs cancel_factors*}
+
+ML {* Addsimprocs Numeral_Simprocs.cancel_factors *}
(* links with rbl operations *)
lemma word_succ_rbl: