* 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.)
- [isabelle-dev] NEWS Florian Haftmann
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Lawrence Paulson
- [isabelle-dev] NEWS Clemens Ballarin
- [isabelle-dev] NEWS Tobias Nipkow
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Gerwin Klein
- [isabelle-dev] NE... Makarius
- [isabelle-dev... Gerwin Klein
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS balla...@mailbroy.informatik.tu-muenchen.de
- [isabelle-dev] NEWS Florian Haftmann
- [isabelle-dev] NEWS Florian Haftmann
- [isabelle-dev] NEWS Tobias Nipkow
- [isabelle-dev] Factorials... Amine Chaieb
- [isabelle-dev] Factor... Tobias Nipkow
- [isabelle-dev] Factor... Lawrence Paulson
- [isabelle-dev] Factor... Florian Haftmann