2010-11-08 haftmann [Mon, 08 Nov 2010 10:43:24 +0100] rev 40421
constructors to datatypes in code_reflect can be globbed; dropped unused code
src/Tools/Code/code_runtime.ML

2010-11-08 bulwahn [Mon, 08 Nov 2010 09:25:43 +0100] rev 40420
adding code and theory for smallvalue generators, but do not setup the interpretation yet
src/HOL/IsaMakefile src/HOL/Main.thy src/HOL/Smallcheck.thy src/HOL/Tools/smallvalue_generators.ML

2010-11-08 blanchet [Mon, 08 Nov 2010 02:33:48 +0100] rev 40419
make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice
src/HOL/Tools/Sledgehammer/sledgehammer.ML

2010-11-08 blanchet [Mon, 08 Nov 2010 02:32:27 +0100] rev 40418
better detection of completely irrelevant facts
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML

2010-11-07 blanchet [Sun, 07 Nov 2010 18:19:04 +0100] rev 40417
always use a hard timeout in Mirabelle
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML src/HOL/Tools/Sledgehammer/sledgehammer.ML

2010-11-07 blanchet [Sun, 07 Nov 2010 18:15:13 +0100] rev 40416
use "smt" (rather than "metis") to reconstruct SMT proofs
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

2010-11-07 blanchet [Sun, 07 Nov 2010 18:03:24 +0100] rev 40415
don't pass too many facts on the first iteration of the SMT solver
src/HOL/Tools/Sledgehammer/sledgehammer.ML

2010-11-07 blanchet [Sun, 07 Nov 2010 18:02:02 +0100] rev 40414
catch TimeOut exception
src/HOL/Tools/Sledgehammer/sledgehammer.ML

2010-11-07 blanchet [Sun, 07 Nov 2010 17:56:07 +0100] rev 40413
ensure the SMT solver respects the timeout -- Mirabelle revealed cases where "smt_filter" apparently never returns
src/HOL/Tools/Sledgehammer/sledgehammer.ML

2010-11-07 blanchet [Sun, 07 Nov 2010 17:51:25 +0100] rev 40412
if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed
src/HOL/Tools/Sledgehammer/sledgehammer.ML