--- a/src/HOL/Hyperreal/Poly.thy Thu Jun 07 01:44:35 2007 +0200
+++ b/src/HOL/Hyperreal/Poly.thy Thu Jun 07 02:34:37 2007 +0200
@@ -403,7 +403,7 @@
apply (cut_tac h = aa and t = list and a = a in poly_linear_rem, safe)
apply (case_tac "q", auto)
apply (drule_tac x = "[]" in spec, simp)
-apply (auto simp add: poly_add poly_cmult real_add_assoc)
+apply (auto simp add: poly_add poly_cmult add_assoc)
apply (drule_tac x = "aa#lista" in spec, auto)
done
--- a/src/HOL/Hyperreal/Transcendental.thy Thu Jun 07 01:44:35 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy Thu Jun 07 02:34:37 2007 +0200
@@ -1075,7 +1075,7 @@
done
lemma sin_cos_squared_add2 [simp]: "((cos x)\<twosuperior>) + ((sin x)\<twosuperior>) = 1"
-apply (subst real_add_commute)
+apply (subst add_commute)
apply (simp (no_asm) del: realpow_Suc)
done
@@ -1547,7 +1547,7 @@
apply (cut_tac y="-y" in cos_total, simp) apply simp
apply (erule ex1E)
apply (rule_tac a = "x - (pi/2)" in ex1I)
-apply (simp (no_asm) add: real_add_assoc)
+apply (simp (no_asm) add: add_assoc)
apply (rotate_tac 3)
apply (drule_tac x = "xa + pi/2" in spec, safe, simp_all)
done