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/Rational.thy
changeset 30649 57753e0ec1d4
parent 30273 ecd6f0ca62ea
child 30960 fec1a04b7220 
--- a/src/HOL/Rational.thy	Sat Mar 21 12:37:13 2009 +0100
+++ b/src/HOL/Rational.thy	Sun Mar 22 19:36:04 2009 +0100
@@ -691,7 +691,6 @@
     \<longleftrightarrow> Fract a b < Fract c d"
     using not_zero `b * d > 0`
     by (simp add: of_rat_rat of_int_divide_less_eq of_int_mult [symmetric] del: of_int_mult)
-      (auto intro: mult_strict_right_mono mult_right_less_imp_less)
 qed
 
 lemma of_rat_less_eq:
isabelle