* HOL: command 'atp_messages' displays recent messages issued by automated theorem provers. This allows to examine results that might have got lost due to the asynchronous nature of default 'sledgehammer' output. (This acknowledges the fact that sledghammer occasionally breaks the Proof General model, which is inherently synchronous.)