--- a/src/HOL/Rat.thy Thu Oct 31 16:54:22 2013 +0100
+++ b/src/HOL/Rat.thy Fri Nov 01 18:51:14 2013 +0100
@@ -468,7 +468,7 @@
unfolding less_eq_rat_def less_rat_def
by (auto, drule (1) positive_add, simp add: positive_zero)
show "a \<le> b \<Longrightarrow> c + a \<le> c + b"
- unfolding less_eq_rat_def less_rat_def by (auto simp: diff_minus)
+ unfolding less_eq_rat_def less_rat_def by auto
show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
by (rule sgn_rat_def)
show "a \<le> b \<or> b \<le> a"
@@ -665,7 +665,7 @@
by transfer simp
lemma of_rat_diff: "of_rat (a - b) = of_rat a - of_rat b"
-by (simp only: diff_minus of_rat_add of_rat_minus)
+ using of_rat_add [of a "- b"] by (simp add: of_rat_minus)
lemma of_rat_mult: "of_rat (a * b) = of_rat a * of_rat b"
apply transfer