Simple-minded technology to record HOL sessions

Intention is to generate Manuals' sessions automatically so that they
won't bitrot (as per issue #325).

My feeling is that this approach should be replaced by something that
directly calls the compiler while sweeping over the TeX sources.