--- a/src/HOL/NSA/HSeries.thy Thu Oct 31 16:54:22 2013 +0100
+++ b/src/HOL/NSA/HSeries.thy Fri Nov 01 18:51:14 2013 +0100
@@ -131,7 +131,7 @@
apply (auto simp add: approx_refl)
apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
apply (auto dest: approx_hrabs
- simp add: sumhr_split_diff diff_minus [symmetric])
+ simp add: sumhr_split_diff)
done
(*----------------------------------------------------------------
@@ -172,7 +172,7 @@
apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
apply (rule_tac [2] approx_minus_iff [THEN iffD2])
apply (auto dest: approx_hrabs_zero_cancel
- simp add: sumhr_split_diff diff_minus [symmetric])
+ simp add: sumhr_split_diff)
done