# HG changeset patch
# User nipkow
# Date 977421459 -3600
# Node ID 439e44031b815c5a6dc336e413f95ca2e1606320
# Parent  55c8367bab058061123938af555442085e0a6a59
something stopped working, had to add real_add_ac

diff -r 55c8367bab05 -r 439e44031b81 src/HOL/Real/Hyperreal/Lim.ML
--- a/src/HOL/Real/Hyperreal/Lim.ML	Thu Dec 21 18:57:12 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Lim.ML	Thu Dec 21 18:57:39 2000 +0100
@@ -1591,7 +1591,7 @@
       simpset() addsimps [eq_divide_2_times_iff, real_add_divide_distrib, 
                           Let_def, split_def]));
 by (auto_tac (claset(), 
-              simpset() addsimps [Bolzano_bisect_le, real_diff_def]));  
+              simpset() addsimps (real_add_ac@[Bolzano_bisect_le, real_diff_def])));
 qed "Bolzano_bisect_diff";
 
 val Bolzano_nest_unique =