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