equal
deleted
inserted
replaced
20 delWrapper, delSWrapper: claset * string -> claset |
20 delWrapper, delSWrapper: claset * string -> claset |
21 getWrapper is renamed to appWrappers, getSWrapper to appSWrappers; |
21 getWrapper is renamed to appWrappers, getSWrapper to appSWrappers; |
22 |
22 |
23 |
23 |
24 *** HOL *** |
24 *** HOL *** |
|
25 |
|
26 * split_all_tac now fails if there is nothing to split |
|
27 split_all_tac has moved within claset() from usafe wrappers to safe wrappers |
25 |
28 |
26 * added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset |
29 * added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset |
27 |
30 |
28 * HOL/Arithmetic: removed 'pred' (predecessor) function; and generalized |
31 * HOL/Arithmetic: removed 'pred' (predecessor) function; and generalized |
29 some theorems about n-1 |
32 some theorems about n-1 |