diff -r 3cf7a067599c -r 112eefe85ff0 NEWS --- 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) -----------------------------------