--- a/src/HOL/Rat.thy Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Rat.thy Sat Apr 12 17:26:27 2014 +0200
@@ -429,7 +429,7 @@
apply transfer
apply (simp add: zero_less_mult_iff)
apply (elim disjE, simp_all add: add_pos_pos add_neg_neg
- mult_pos_pos mult_pos_neg mult_neg_pos mult_neg_neg)
+ mult_pos_neg mult_neg_pos mult_neg_neg)
done
lemma positive_mult:
@@ -726,7 +726,7 @@
proof (induct r, induct s)
fix a b c d :: int
assume not_zero: "b > 0" "d > 0"
- then have "b * d > 0" by (rule mult_pos_pos)
+ then have "b * d > 0" by simp
have of_int_divide_less_eq:
"(of_int a :: 'a) / of_int b < of_int c / of_int d
\<longleftrightarrow> (of_int a :: 'a) * of_int d < of_int c * of_int b"