Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
something stopped working, had to add real_add_ac
authornipkow
Thu, 21 Dec 2000 18:57:39 +0100
changeset 10723 439e44031b81
parent 10722 55c8367bab05
child 10724 819ee80305a8
something stopped working, had to add real_add_ac
src/HOL/Real/Hyperreal/Lim.ML file | annotate | diff | comparison | revisions 
--- 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 =
isabelle