author | haftmann |
Wed, 21 Nov 2007 13:42:31 +0100 | |
changeset 25450 | c3b26e533b21 |
parent 25449 | f3d5111a9c4b |
child 25451 | 7bd190cac91e |
--- 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