Check the expected behavior in the examples of Help/*.hlp #139
Description
It would be great if HOL Light's continuous integration monthly checks whether there is any discrepancy between the expected output of examples in Help/*.hlp and their actual output.
A question is whether it will fit in the resources of our CI budget. I need to measure its running time for a precise answer (storage space will be fine), but my two cents is that the resource will be enough.