# HG changeset patch # User haftmann # Date 1195648951 -3600 # Node ID c3b26e533b21c2f4fc066a86c1399e97c2733eaa # Parent f3d5111a9c4bd045db8d8290d49ef1f8b4e6da3b dropped diagnostic commands diff -r f3d5111a9c4b -r c3b26e533b21 src/HOL/Ring_and_Field.thy --- 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