diff -r 5f8643e8ced5 -r 52235c27538c NEWS
--- a/NEWS	Tue Sep 06 21:36:48 2016 +0200
+++ b/NEWS	Wed Sep 07 22:28:30 2016 +0200
@@ -66,7 +66,15 @@
 is relevant to avoid confusion of Pure.simp vs. HOL.simp.
 
 * Commands 'prf' and 'full_prf' are somewhat more informative (again):
-proof terms are reconstructed and cleaned from administrative thm nodes.
+proof terms are reconstructed and cleaned from administrative thm
+nodes.
+
+* The command 'unfolding' and proof method "unfold" include a second
+stage where given equations are passed through the attribute "abs_def"
+before rewriting. This ensures that definitions are fully expanded,
+regardless of the actual parameters that are provided. Rare
+INCOMPATIBILITY in some corner cases: use proof method (simp only:)
+instead, or declare [[unfold_abs_def = false]] in the proof context.
 
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***