Thu, 09 Sep 2010 16:06:11 +0200 better error reporting when the Sledgehammer minimizer is interrupted
blanchet [Thu, 09 Sep 2010 16:06:11 +0200] rev 39262
better error reporting when the Sledgehammer minimizer is interrupted
Thu, 09 Sep 2010 14:47:06 +0200 add cutoff beyond which facts are handled using definitional CNF
blanchet [Thu, 09 Sep 2010 14:47:06 +0200] rev 39261
add cutoff beyond which facts are handled using definitional CNF
Thu, 09 Sep 2010 12:28:00 +0200 "resurrected" a Metis proof
blanchet [Thu, 09 Sep 2010 12:28:00 +0200] rev 39260
"resurrected" a Metis proof
Thu, 09 Sep 2010 12:24:43 +0200 replace two slow "metis" proofs with faster proofs
blanchet [Thu, 09 Sep 2010 12:24:43 +0200] rev 39259
replace two slow "metis" proofs with faster proofs
Wed, 08 Sep 2010 19:22:37 +0200 workaround to avoid subtle "add_ffpairs" unification exception in Sledgehammer;
blanchet [Wed, 08 Sep 2010 19:22:37 +0200] rev 39258
workaround to avoid subtle "add_ffpairs" unification exception in Sledgehammer; to reproduce the old bug, replace the command by(rule new_Addr_SomeD) on line 27 of Jinja/J/TypeSafe.thy with by (metis new_Addr_SomeD)
Wed, 08 Sep 2010 19:20:52 +0200 improve SInE-E failure message
blanchet [Wed, 08 Sep 2010 19:20:52 +0200] rev 39257
improve SInE-E failure message
Thu, 09 Sep 2010 17:58:11 +0200 merged
bulwahn [Thu, 09 Sep 2010 17:58:11 +0200] rev 39256
merged
Thu, 09 Sep 2010 17:23:08 +0200 adding an example with integers and String.literals
bulwahn [Thu, 09 Sep 2010 17:23:08 +0200] rev 39255
adding an example with integers and String.literals
Thu, 09 Sep 2010 17:23:07 +0200 adding an example to show how code_pred must be invoked with locales
bulwahn [Thu, 09 Sep 2010 17:23:07 +0200] rev 39254
adding an example to show how code_pred must be invoked with locales
Thu, 09 Sep 2010 17:23:03 +0200 removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
bulwahn [Thu, 09 Sep 2010 17:23:03 +0200] rev 39253
removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip