tuned;
authorwenzelm
Tue Feb 26 20:09:25 2013 +0100 (2013-02-26)
changeset 5128644a521ff87cf
parent 51285 0859bd338c9b
child 51287 8799eadf61fb
tuned;
src/HOL/Word/Word.thy
     1.1 --- a/src/HOL/Word/Word.thy	Tue Feb 26 19:58:27 2013 +0100
     1.2 +++ b/src/HOL/Word/Word.thy	Tue Feb 26 20:09:25 2013 +0100
     1.3 @@ -1644,11 +1644,10 @@
     1.4    apply (erule (2) udvd_decr0)
     1.5    done
     1.6  
     1.7 -ML {* Delsimprocs [@{simproc linordered_ring_less_cancel_factor}] *}
     1.8 -
     1.9  lemma udvd_incr2_K: 
    1.10    "p < a + s \<Longrightarrow> a <= a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a <= p \<Longrightarrow> 
    1.11      0 < K \<Longrightarrow> p <= p + K & p + K <= a + s"
    1.12 +  using [[simproc del: linordered_ring_less_cancel_factor]]
    1.13    apply (unfold udvd_def)
    1.14    apply clarify
    1.15    apply (simp add: uint_arith_simps split: split_if_asm)
    1.16 @@ -1662,8 +1661,6 @@
    1.17    apply simp
    1.18    done
    1.19  
    1.20 -ML {* Addsimprocs [@{simproc linordered_ring_less_cancel_factor}] *}
    1.21 -
    1.22  (* links with rbl operations *)
    1.23  lemma word_succ_rbl:
    1.24    "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = (rev (rbl_succ (rev bl)))"