[isabelle-dev] NEWS

[Alexander Krauss]

Following recent discussion:

* Congruence rules Option.map_cong and Option.bind_cong for recursion
through option types.

This is merely to make sure that HOL is "closed under tool setup" as far 
as reasonably possible. Further constants like mapM should go somewhere 
else. I think that a "Library for Monadic Programming" would make an 
excellent AFP entry... But this requires some polishing of all the 
existing bits and pieces.

Alex