--- a/NEWS Tue Feb 20 18:53:28 2001 +0100
+++ b/NEWS Wed Feb 21 12:07:00 2001 +0100
@@ -1,6 +1,8 @@
Isabelle NEWS -- history user-relevant changes
==============================================
+* HOL: added safe wrapper "split_conv_tac" to claset. EXISTING PROOFS MAY FAIL
+
* HOL: made split_all_tac safe. EXISTING PROOFS MAY FAIL OR LOOP, so in this
(rare) case use delSWrapper "split_all_tac" addSbefore
("unsafe_split_all_tac", unsafe_split_all_tac)
--- a/src/HOL/Hyperreal/Lim.ML Tue Feb 20 18:53:28 2001 +0100
+++ b/src/HOL/Hyperreal/Lim.ML Wed Feb 21 12:07:00 2001 +0100
@@ -1720,6 +1720,7 @@
Addsimps [abs_add_one_not_less_self];
+claset_ref() := claset() delSWrapper "split_conv_tac";
Goal "[| a <= b; ALL x. a <= x & x <= b --> isCont f x |]\
\ ==> EX M. ALL x. a <= x & x <= b --> f(x) <= M";
by (cut_inst_tac [("P","%(u,v). a <= u & u <= v & v <= b --> \
@@ -1764,6 +1765,7 @@
by (auto_tac (claset(),
simpset() addsimps [real_abs_def] addsplits [split_if_asm]));
qed "isCont_bounded";
+claset_ref() := claset() addSbefore ("split_conv_tac", split_conv_tac);
(*----------------------------------------------------------------------------*)
(* Refine the above to existence of least upper bound *)