src/HOL/Rat.thy
changeset 54230 b1d955791529
parent 53652 18fbca265e2e
child 54409 2e501a90dec7
     1.1 --- a/src/HOL/Rat.thy	Thu Oct 31 16:54:22 2013 +0100
     1.2 +++ b/src/HOL/Rat.thy	Fri Nov 01 18:51:14 2013 +0100
     1.3 @@ -468,7 +468,7 @@
     1.4      unfolding less_eq_rat_def less_rat_def
     1.5      by (auto, drule (1) positive_add, simp add: positive_zero)
     1.6    show "a \<le> b \<Longrightarrow> c + a \<le> c + b"
     1.7 -    unfolding less_eq_rat_def less_rat_def by (auto simp: diff_minus)
     1.8 +    unfolding less_eq_rat_def less_rat_def by auto
     1.9    show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
    1.10      by (rule sgn_rat_def)
    1.11    show "a \<le> b \<or> b \<le> a"
    1.12 @@ -665,7 +665,7 @@
    1.13    by transfer simp
    1.14  
    1.15  lemma of_rat_diff: "of_rat (a - b) = of_rat a - of_rat b"
    1.16 -by (simp only: diff_minus of_rat_add of_rat_minus)
    1.17 +  using of_rat_add [of a "- b"] by (simp add: of_rat_minus)
    1.18  
    1.19  lemma of_rat_mult: "of_rat (a * b) = of_rat a * of_rat b"
    1.20  apply transfer