# HG changeset patch
# User huffman
# Date 1181176477 -7200
# Node ID 85e7e043b980c6cd885e334a35195d8f7b8e246f
# Parent  c95a4f6b3881ec08b5823915d3c3cdc530541f9e
tuned

diff -r c95a4f6b3881 -r 85e7e043b980 src/HOL/Hyperreal/Poly.thy
--- 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
 
diff -r c95a4f6b3881 -r 85e7e043b980 src/HOL/Hyperreal/Transcendental.thy
--- 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