2015-10-06 blanchet [Tue, 06 Oct 2015 11:50:23 +0200] rev 61333
compile
src/HOL/Library/Multiset.thy src/HOL/Tools/Nitpick/nitpick_model.ML

2015-10-06 blanchet [Tue, 06 Oct 2015 11:34:07 +0200] rev 61332
tuning
src/HOL/Tools/prop_logic.ML

2015-10-06 blanchet [Tue, 06 Oct 2015 09:27:31 +0200] rev 61331
avoid legacy syntax
src/HOL/Tools/Nitpick/nitpick_model.ML

2015-10-05 blanchet [Mon, 05 Oct 2015 23:03:50 +0200] rev 61330
further improved fine point w.r.t. replaying in the presence of chained facts and a non-empty meta-quantifier prefix + avoid printing internal names in backquotes
src/HOL/Tools/Sledgehammer/sledgehammer.ML src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML src/HOL/Tools/Sledgehammer/sledgehammer_util.ML

2015-10-05 blanchet [Mon, 05 Oct 2015 21:46:48 +0200] rev 61329
added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs
src/HOL/Tools/ATP/atp_problem_generate.ML src/HOL/Tools/ATP/atp_proof.ML src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML

2015-10-05 wenzelm [Mon, 05 Oct 2015 18:03:58 +0200] rev 61328
merged

2015-10-05 wenzelm [Mon, 05 Oct 2015 18:03:52 +0200] rev 61327
tuned signature;
src/Provers/classical.ML

2015-10-05 wenzelm [Mon, 05 Oct 2015 14:17:20 +0200] rev 61326
produce nodes_status outside GUI thread, to avoid a few milliseconds of blocking;
src/Tools/jEdit/src/theories_dockable.scala

2015-10-05 blanchet [Mon, 05 Oct 2015 16:14:33 +0200] rev 61325
avoid too aggressive optimization of 'finite' predicate
NEWS src/HOL/Tools/Nitpick/nitpick_kodkod.ML

2015-10-05 blanchet [Mon, 05 Oct 2015 15:57:25 +0200] rev 61324
avoid unsound simplification of (C (s x)) when s is a selector but not C's
NEWS src/HOL/Tools/Nitpick/nitpick_hol.ML src/HOL/Tools/Nitpick/nitpick_model.ML src/HOL/Tools/Nitpick/nitpick_nut.ML src/HOL/Tools/Nitpick/nitpick_preproc.ML