krauss at in.tum.de
Sat Feb 18 23:44:57 CET 2012
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.
More information about the isabelle-dev