made split_all_tac safe introducing safe_full_simp_tac, EXISTING PROOFS MAY FAIL
authoroheimb
Tue Feb 20 18:47:34 2001 +0100 (2001-02-20)
changeset 1116998c2f741e32b
parent 11168 b964accc9307
child 11170 015af2fc7026
made split_all_tac safe introducing safe_full_simp_tac, EXISTING PROOFS MAY FAIL
NEWS
     1.1 --- a/NEWS	Tue Feb 20 18:47:32 2001 +0100
     1.2 +++ b/NEWS	Tue Feb 20 18:47:34 2001 +0100
     1.3 @@ -1,7 +1,11 @@
     1.4 -
     1.5  Isabelle NEWS -- history user-relevant changes
     1.6  ==============================================
     1.7  
     1.8 +* HOL: made split_all_tac safe. EXISTING PROOFS MAY FAIL OR LOOP, so in this
     1.9 +  (rare) case use   delSWrapper "split_all_tac" addSbefore 
    1.10 +                    ("unsafe_split_all_tac", unsafe_split_all_tac)
    1.11 +
    1.12 +
    1.13  New in Isabelle99-2 (February 2001)
    1.14  -----------------------------------
    1.15