changeset 49962 | a8cc904a6820 |
parent 47171 | 80c432404204 |
child 51301 | 6822aa82aafa |
--- a/src/HOL/Word/Misc_Numeric.thy Fri Oct 19 10:46:42 2012 +0200 +++ b/src/HOL/Word/Misc_Numeric.thy Fri Oct 19 15:12:52 2012 +0200 @@ -301,7 +301,7 @@ apply assumption done -lemmas less_le_mult = less_le_mult' [simplified left_distrib, simplified] +lemmas less_le_mult = less_le_mult' [simplified distrib_right, simplified] lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult, simplified left_diff_distrib]