# HG changeset patch
# User oheimb
# Date 891513572 -7200
# Node ID 9658aab68363e5ed2e11453687298df11a576de9
# Parent  d2c41c8b545f356a974365baf4683315ac0a6671
*** empty log message ***

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