isabelle: Changelog

blanchet [Fri, 27 May 2011 10:30:07 +0200] rev 43008

renamed "minimize" to "min" to make Sledgehammer output a little bit more concise

blanchet [Fri, 27 May 2011 10:30:07 +0200] rev 43007

minor doc adjustments

blanchet [Fri, 27 May 2011 10:30:07 +0200] rev 43006

make output more concise

blanchet [Fri, 27 May 2011 10:30:07 +0200] rev 43005

merge timeout messages from several ATPs into one message to avoid clutter

blanchet [Fri, 27 May 2011 10:30:07 +0200] rev 43004

fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context

blanchet [Fri, 27 May 2011 10:30:07 +0200] rev 43003

tuning

blanchet [Fri, 27 May 2011 10:30:07 +0200] rev 43002

mention contributions from LCP and explain metis and metisFT encodings

blanchet [Fri, 27 May 2011 10:30:07 +0200] rev 43001

fixed trivial fact detection

blanchet [Fri, 27 May 2011 10:30:07 +0200] rev 43000

cleaner handling of equality and proxies (esp. for THF)

blanchet [Fri, 27 May 2011 10:30:07 +0200] rev 42999

recognize more ATP failures

isabelle