2012-02-05 bulwahn [Sun, 05 Feb 2012 08:24:39 +0100] rev 46418
another try to improve code generation of set equality (cf. da32cf32c0c7)
src/HOL/List.thy

2012-02-05 bulwahn [Sun, 05 Feb 2012 08:24:38 +0100] rev 46417
beautifying definitions of check_all and adding instance for finite_4
src/HOL/Quickcheck_Exhaustive.thy

2012-02-05 Cezary Kaliszyk <cezarykaliszyk@gmail.com> [Sun, 05 Feb 2012 07:05:34 +0100] rev 46416
Make automatic derivation of raw/quotient types more greedy to allow descending and quot_lifted for compound quotients.
src/HOL/Quotient_Examples/FSet.thy src/HOL/Tools/Quotient/quotient_term.ML

2012-02-04 blanchet [Sat, 04 Feb 2012 17:01:25 +0100] rev 46415
added option to Mirabelle/Sledgehammer
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

2012-02-04 blanchet [Sat, 04 Feb 2012 12:08:18 +0100] rev 46414
improved hashing w.r.t. Mirabelle, to help debugging
src/HOL/Tools/ATP/atp_problem.ML

2012-02-04 blanchet [Sat, 04 Feb 2012 12:08:18 +0100] rev 46413
tuned SPASS DFG output
src/HOL/Tools/ATP/atp_problem.ML

2012-02-04 blanchet [Sat, 04 Feb 2012 12:08:18 +0100] rev 46412
the new SPASS gives accurate fact information, so no need for old hack anymore
src/HOL/Tools/ATP/scripts/spass_new

2012-02-04 blanchet [Sat, 04 Feb 2012 12:08:18 +0100] rev 46411
fixed docs
doc-src/Sledgehammer/sledgehammer.tex

2012-02-04 blanchet [Sat, 04 Feb 2012 12:08:18 +0100] rev 46410
made sure to filter type args also for "uncurried alias" equations
src/HOL/Tools/ATP/atp_problem_generate.ML

2012-02-04 blanchet [Sat, 04 Feb 2012 12:08:18 +0100] rev 46409
made option available to users (mostly for experiments)
NEWS doc-src/Sledgehammer/sledgehammer.tex src/HOL/TPTP/atp_theory_export.ML src/HOL/Tools/ATP/atp_problem_generate.ML src/HOL/Tools/ATP/atp_systems.ML src/HOL/Tools/Metis/metis_generate.ML src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML src/HOL/Tools/Sledgehammer/sledgehammer_run.ML