1.1 --- a/NEWS	Mon Mar 30 21:15:18 1998 +0200
     1.2 +++ b/NEWS	Thu Apr 02 12:39:32 1998 +0200
     1.3 @@ -23,6 +23,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* split_all_tac now fails if there is nothing to split
     1.8 +  split_all_tac has moved within claset() from usafe wrappers to safe wrappers
     1.9 +
    1.10  * added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset
    1.11  
    1.12  * HOL/Arithmetic: removed 'pred' (predecessor) function; and generalized