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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
