# HG changeset patch
# User wenzelm
# Date 1361905765 -3600
# Node ID 44a521ff87cfb528870e4cc11b99753094162e0a
# Parent  0859bd338c9bedb915833a0c6a535e03b80a5a63
tuned;

diff -r 0859bd338c9b -r 44a521ff87cf src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Tue Feb 26 19:58:27 2013 +0100
+++ b/src/HOL/Word/Word.thy	Tue Feb 26 20:09:25 2013 +0100
@@ -1644,11 +1644,10 @@
   apply (erule (2) udvd_decr0)
   done
 
-ML {* Delsimprocs [@{simproc linordered_ring_less_cancel_factor}] *}
-
 lemma udvd_incr2_K: 
   "p < a + s \<Longrightarrow> a <= a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a <= p \<Longrightarrow> 
     0 < K \<Longrightarrow> p <= p + K & p + K <= a + s"
+  using [[simproc del: linordered_ring_less_cancel_factor]]
   apply (unfold udvd_def)
   apply clarify
   apply (simp add: uint_arith_simps split: split_if_asm)
@@ -1662,8 +1661,6 @@
   apply simp
   done
 
-ML {* Addsimprocs [@{simproc linordered_ring_less_cancel_factor}] *}
-
 (* links with rbl operations *)
 lemma word_succ_rbl:
   "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = (rev (rbl_succ (rev bl)))"