changeset 25450 | c3b26e533b21 |
parent 25304 | 7491c00f0915 |
child 25512 | 4134f7c782e2 |
--- a/src/HOL/Ring_and_Field.thy Tue Nov 20 14:01:49 2007 +0100 +++ b/src/HOL/Ring_and_Field.thy Wed Nov 21 13:42:31 2007 +0100 @@ -1930,8 +1930,6 @@ apply simp apply (subst times_divide_eq_left) apply (rule mult_imp_le_div_pos, assumption) - thm mult_mono - thm mult_mono' apply (rule mult_mono) apply simp_all done