changeset 62327 | 112eefe85ff0 |
parent 62312 | 5e5a881ebc12 |
child 62332 | eeaa2f7b5329 |
--- a/NEWS Wed Feb 17 11:54:34 2016 +0100 +++ b/NEWS Wed Feb 17 12:07:49 2016 +0100 @@ -13,6 +13,13 @@ typesetting. E.g. to produce proof holes in examples and documentation. +*** HOL *** + +* (Co)datatype package: + - "primrec" now allows nested calls through the predicator in addition + to the map function. + + New in Isabelle2016 (February 2016) -----------------------------------