2010-09-14 blanchet [Tue, 14 Sep 2010 17:36:27 +0200] rev 39368
generalize proof reconstruction code;
first step towards support for nonnumeric formula names, needed for E 1.2
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML

2010-09-14 blanchet [Tue, 14 Sep 2010 17:23:16 +0200] rev 39367
tuning
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML

2010-09-14 blanchet [Tue, 14 Sep 2010 16:34:26 +0200] rev 39366
handle relevance filter corner cases more gracefully;
e.g. the minimizer selects 15 facts but "max_relevant = 14"
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML src/HOL/Tools/Sledgehammer/sledgehammer.ML src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML

2010-09-14 blanchet [Tue, 14 Sep 2010 16:33:38 +0200] rev 39365
remove more clutter related to old "fast_descrs" optimization
src/HOL/Nitpick.thy

2010-09-14 blanchet [Tue, 14 Sep 2010 15:39:57 +0200] rev 39364
Sledgehammer should be called in "prove" mode;
otherwise the proof text won't fit into the proof document
src/HOL/Tools/Sledgehammer/sledgehammer.ML

2010-09-14 blanchet [Tue, 14 Sep 2010 14:47:53 +0200] rev 39363
added a timeout around "try" call in Mirabelle
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

2010-09-14 blanchet [Tue, 14 Sep 2010 14:22:49 +0200] rev 39362
adapt examples to latest Nitpick changes + speed them up a little bit
src/HOL/Nitpick_Examples/Integer_Nits.thy src/HOL/Nitpick_Examples/Manual_Nits.thy src/HOL/Nitpick_Examples/Typedef_Nits.thy

2010-09-14 blanchet [Tue, 14 Sep 2010 14:12:18 +0200] rev 39361
tuning
src/HOL/Tools/Nitpick/nitpick.ML

2010-09-14 blanchet [Tue, 14 Sep 2010 13:44:43 +0200] rev 39360
eliminate more clutter related to "fast_descrs" optimization
src/HOL/Tools/Nitpick/nitpick_hol.ML src/HOL/Tools/Nitpick/nitpick_kodkod.ML src/HOL/Tools/Nitpick/nitpick_model.ML src/HOL/Tools/Nitpick/nitpick_mono.ML src/HOL/Tools/Nitpick/nitpick_nut.ML src/HOL/Tools/Nitpick/nitpick_preproc.ML

2010-09-14 blanchet [Tue, 14 Sep 2010 13:24:18 +0200] rev 39359
remove "fast_descs" option from Nitpick;
the option has been unsound for over a year and is too imprecise to be of any use when made sound
doc-src/Nitpick/nitpick.tex src/HOL/Nitpick_Examples/Core_Nits.thy src/HOL/Nitpick_Examples/Mono_Nits.thy src/HOL/Tools/Nitpick/nitpick.ML src/HOL/Tools/Nitpick/nitpick_hol.ML src/HOL/Tools/Nitpick/nitpick_isar.ML src/HOL/Tools/Nitpick/nitpick_model.ML src/HOL/Tools/Nitpick/nitpick_mono.ML src/HOL/Tools/Nitpick/nitpick_nut.ML src/HOL/Tools/Nitpick/nitpick_preproc.ML