--- a/NEWS Sun Sep 06 19:09:20 2015 +0200
+++ b/NEWS Sun Sep 06 21:55:13 2015 +0200
@@ -282,6 +282,11 @@
* Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef'
command. Minor INCOMPATIBILITY, use 'function' instead.
+* Recursive function definitions ('fun', 'function', 'partial_function')
+no longer expose the low-level "_def" facts of the internal
+construction. INCOMPATIBILITY, enable option "function_defs" in the
+context for rare situations where these facts are really needed.
+
* Imperative_HOL: obsolete theory Legacy_Mrec has been removed.