| changeset 34962 | 807f6ce0273d |
| parent 34946 | aa5d27f1d9b9 |
| child 34974 | 18b41bba42b5 |
| child 36093 | 0880493627ca |
--- a/NEWS Fri Jan 22 13:39:00 2010 +0100 +++ b/NEWS Fri Jan 22 16:56:51 2010 +0100 @@ -12,6 +12,9 @@ *** HOL *** +* HOLogic.strip_psplit: types are returned in syntactic order, similar +to other strip and tuple operations. INCOMPATIBILITY. + * Various old-style primrec specifications in the HOL theories have been replaced by new-style primrec, especially in theory List. The corresponding constants now have authentic syntax. INCOMPATIBILITY.