Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Ring_and_Field.thy
changeset 25450 c3b26e533b21
parent 25304 7491c00f0915
child 25512 4134f7c782e2 
--- 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
isabelle