1.1 --- a/src/HOL/Ring_and_Field.thy	Tue Nov 20 14:01:49 2007 +0100
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Wed Nov 21 13:42:31 2007 +0100
     1.3 @@ -1930,8 +1930,6 @@
     1.4    apply simp
     1.5    apply (subst times_divide_eq_left)
     1.6    apply (rule mult_imp_le_div_pos, assumption)
     1.7 -  thm mult_mono
     1.8 -  thm mult_mono'
     1.9    apply (rule mult_mono)
    1.10    apply simp_all
    1.11  done