[isabelle-dev] NEWS

Makarius makarius at sketis.net
Mon Dec 15 22:10:51 CET 2008

* 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.)

More information about the isabelle-dev mailing list