# HG changeset patch
# User oheimb
# Date 982691254 -3600
# Node ID 98c2f741e32bfecff412e3ef26cd750bde463fff
# Parent  b964accc93074946d26a4478369270e89694be6d
made split_all_tac safe introducing safe_full_simp_tac, EXISTING PROOFS MAY FAIL

diff -r b964accc9307 -r 98c2f741e32b NEWS
--- a/NEWS	Tue Feb 20 18:47:32 2001 +0100
+++ b/NEWS	Tue Feb 20 18:47:34 2001 +0100
@@ -1,7 +1,11 @@
-
 Isabelle NEWS -- history user-relevant changes
 ==============================================
 
+* 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)
+
+
 New in Isabelle99-2 (February 2001)
 -----------------------------------