# 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