# HG changeset patch
# User krauss
# Date 1329602731 -3600
# Node ID 1bbee2041321a10e8418c796d6c23ca513b1c224
# Parent  274bb026da6c7239af85ba964b5fcfffea48a57a
NEWS

diff -r 274bb026da6c -r 1bbee2041321 NEWS
--- a/NEWS	Sat Feb 18 22:31:24 2012 +0100
+++ b/NEWS	Sat Feb 18 23:05:31 2012 +0100
@@ -126,6 +126,9 @@
 and "foldl_def".  For the common phrases "%xs. List.foldr plus xs 0"
 and "List.foldl plus 0", prefer "List.listsum".
 
+* Congruence rules Option.map_cong and Option.bind_cong for recursion
+through option types.
+
 * 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