made split_all_tac safe introducing safe_full_simp_tac, EXISTING PROOFS MAY FAIL
authoroheimb
Tue, 20 Feb 2001 18:47:34 +0100
changeset 11169 98c2f741e32b
parent 11168 b964accc9307
child 11170 015af2fc7026
made split_all_tac safe introducing safe_full_simp_tac, EXISTING PROOFS MAY FAIL
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)
 -----------------------------------