diff -r 487d764fca4a -r 1a474286f315 NEWS
--- a/NEWS	Mon Jul 04 19:46:19 2016 +0200
+++ b/NEWS	Mon Jul 04 19:46:19 2016 +0200
@@ -136,6 +136,9 @@
 
 *** HOL ***
 
+* Locale bijection establishes convenient default simp rules
+like "inv f (f a) = a" for total bijections.
+
 * Former locale lifting_syntax is now a bundle, which is easier to
 include in a local context or theorem statement, e.g. "context includes
 lifting_syntax begin ... end". Minor INCOMPATIBILITY.