1.1 --- a/NEWS	Tue Feb 20 18:53:28 2001 +0100
     1.2 +++ b/NEWS	Wed Feb 21 12:07:00 2001 +0100
     1.3 @@ -1,6 +1,8 @@
     1.4  Isabelle NEWS -- history user-relevant changes
     1.5  ==============================================
     1.6  
     1.7 +* HOL: added safe wrapper "split_conv_tac" to claset. EXISTING PROOFS MAY FAIL
     1.8 +
     1.9  * HOL: made split_all_tac safe. EXISTING PROOFS MAY FAIL OR LOOP, so in this
    1.10    (rare) case use   delSWrapper "split_all_tac" addSbefore 
    1.11                      ("unsafe_split_all_tac", unsafe_split_all_tac)

     2.1 --- a/src/HOL/Hyperreal/Lim.ML	Tue Feb 20 18:53:28 2001 +0100
     2.2 +++ b/src/HOL/Hyperreal/Lim.ML	Wed Feb 21 12:07:00 2001 +0100
     2.3 @@ -1720,6 +1720,7 @@
     2.4  Addsimps [abs_add_one_not_less_self];
     2.5  
     2.6  
     2.7 +claset_ref() := claset() delSWrapper "split_conv_tac";
     2.8  Goal "[| a <= b; ALL x. a <= x & x <= b --> isCont f x |]\
     2.9  \     ==> EX M. ALL x. a <= x & x <= b --> f(x) <= M";
    2.10  by (cut_inst_tac [("P","%(u,v). a <= u & u <= v & v <= b --> \
    2.11 @@ -1764,6 +1765,7 @@
    2.12  by (auto_tac (claset(),
    2.13                simpset() addsimps [real_abs_def] addsplits [split_if_asm]));
    2.14  qed "isCont_bounded";
    2.15 +claset_ref() := claset() addSbefore ("split_conv_tac", split_conv_tac);
    2.16  
    2.17  (*----------------------------------------------------------------------------*)
    2.18  (* Refine the above to existence of least upper bound                         *)