diff -r 3ee75fe01986 -r 00cd193a48dc NEWS
--- a/NEWS	Thu Jan 05 15:31:49 2012 +0100
+++ b/NEWS	Thu Jan 05 18:18:39 2012 +0100
@@ -60,6 +60,12 @@
 
 *** HOL ***
 
+* Concrete syntax for case expressions includes constraints for source
+positions, and thus produces Prover IDE markup for its bindings.
+INCOMPATIBILITY for old-style syntax translations that augment the
+pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of
+one_case.
+
 * Finite_Set.fold now qualified.  INCOMPATIBILITY.
 
 * Renamed some facts on canonical fold on lists, in order to avoid problems