src/HOL/Rat.thy
changeset 56571 f4635657d66f
parent 56544 b60d5d119489
child 57136 653e56c6c963
     1.1 --- a/src/HOL/Rat.thy	Mon Apr 14 10:55:56 2014 +0200
     1.2 +++ b/src/HOL/Rat.thy	Mon Apr 14 13:08:17 2014 +0200
     1.3 @@ -578,7 +578,7 @@
     1.4      by (cases "b = 0", simp, simp add: of_int_rat)
     1.5    moreover have "0 \<le> Fract (a mod b) b \<and> Fract (a mod b) b < 1"
     1.6      unfolding Fract_of_int_quotient
     1.7 -    by (rule linorder_cases [of b 0]) (simp add: divide_nonpos_neg, simp, simp add: divide_nonneg_pos)
     1.8 +    by (rule linorder_cases [of b 0]) (simp_all add: divide_nonpos_neg)
     1.9    ultimately show ?thesis by simp
    1.10  qed
    1.11