# HG changeset patch # User haftmann # Date 1241782701 -7200 # Node ID 796d3d42c87373cf3026ca077157887a1c1f400d # Parent 845a6acd3bf363fb04b4572847e63e8a988b3ed3 proper structure name diff -r 845a6acd3bf3 -r 796d3d42c873 src/HOL/Word/WordArith.thy --- 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: