diff -r 1409b4015671 -r be2d9f5ddc76 NEWS --- a/NEWS Fri Jun 19 19:45:01 2015 +0200 +++ b/NEWS Fri Jun 19 20:14:50 2015 +0200 @@ -129,6 +129,9 @@ less_eq_multiset_def INCOMPATIBILITY +* Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef' +command. Minor INCOMPATIBILITY, use 'function' instead. + New in Isabelle2015 (May 2015)