NEWS
changeset 46528 1bbee2041321
parent 46512 4f9f61f9b535
child 46591 1116909ef176
     1.1 --- a/NEWS	Sat Feb 18 22:31:24 2012 +0100
     1.2 +++ b/NEWS	Sat Feb 18 23:05:31 2012 +0100
     1.3 @@ -126,6 +126,9 @@
     1.4  and "foldl_def".  For the common phrases "%xs. List.foldr plus xs 0"
     1.5  and "List.foldl plus 0", prefer "List.listsum".
     1.6  
     1.7 +* Congruence rules Option.map_cong and Option.bind_cong for recursion
     1.8 +through option types.
     1.9 +
    1.10  * Concrete syntax for case expressions includes constraints for source
    1.11  positions, and thus produces Prover IDE markup for its bindings.
    1.12  INCOMPATIBILITY for old-style syntax translations that augment the