NEWS

--- a/NEWS	Thu Dec 08 15:21:18 2016 +0100
+++ b/NEWS	Thu Dec 08 17:22:51 2016 +0100
@@ -11,7 +11,9 @@
     with type class annotations. As a result, the tactic that derives
     it no longer fails on nested datatypes. Slight INCOMPATIBILITY.
 
-
+* The theorem in Permutations has been renamed:
+  bij_swap_ompose_bij ~> bij_swap_compose_bij
+ 
 
 New in Isabelle2016-1 (December 2016)
 -------------------------------------