changeset 26072 | f65a7fa2da6c |
parent 25937 | 6e5b0f176dac |
child 26086 | 3c243098b64a |
--- a/src/HOL/Word/Num_Lemmas.thy Fri Feb 15 16:09:10 2008 +0100 +++ b/src/HOL/Word/Num_Lemmas.thy Fri Feb 15 16:09:12 2008 +0100 @@ -535,7 +535,7 @@ apply (erule th2) done -lemmas td_gal_lt = td_gal [simplified le_def, simplified] +lemmas td_gal_lt = td_gal [simplified not_less [symmetric], simplified] lemma div_mult_le: "(a :: nat) div b * b <= a" apply (cases b)