src/HOL/Rat.thy
changeset 56544 b60d5d119489
parent 56479 91958d4b30f7
child 56571 f4635657d66f
     1.1 --- a/src/HOL/Rat.thy	Fri Apr 11 23:22:00 2014 +0200
     1.2 +++ b/src/HOL/Rat.thy	Sat Apr 12 17:26:27 2014 +0200
     1.3 @@ -429,7 +429,7 @@
     1.4  apply transfer
     1.5  apply (simp add: zero_less_mult_iff)
     1.6  apply (elim disjE, simp_all add: add_pos_pos add_neg_neg
     1.7 -  mult_pos_pos mult_pos_neg mult_neg_pos mult_neg_neg)
     1.8 +  mult_pos_neg mult_neg_pos mult_neg_neg)
     1.9  done
    1.10  
    1.11  lemma positive_mult:
    1.12 @@ -726,7 +726,7 @@
    1.13  proof (induct r, induct s)
    1.14    fix a b c d :: int
    1.15    assume not_zero: "b > 0" "d > 0"
    1.16 -  then have "b * d > 0" by (rule mult_pos_pos)
    1.17 +  then have "b * d > 0" by simp
    1.18    have of_int_divide_less_eq:
    1.19      "(of_int a :: 'a) / of_int b < of_int c / of_int d
    1.20        \<longleftrightarrow> (of_int a :: 'a) * of_int d < of_int c * of_int b"