# HG changeset patch
# User oheimb
# Date 982753620 -3600
# Node ID 3c82b641b642d0ce8cb32b02f09fdc9d35c47ee0
# Parent  8aa53b4591a53bd2adbe1519f6637aa68734e4a1
added split_conv_tac (also to claset()) as an optimization

diff -r 8aa53b4591a5 -r 3c82b641b642 NEWS
--- 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)
diff -r 8aa53b4591a5 -r 3c82b641b642 src/HOL/Hyperreal/Lim.ML
--- 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                         *)