author | oheimb |
Thu, 02 Apr 1998 12:39:32 +0200 | |
changeset 4766 | 9658aab68363 |
parent 4765 | d2c41c8b545f |
child 4767 | b9f3468c6ee2 |
--- 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