# 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