2014-06-22 sultana [Sun, 22 Jun 2014 06:16:57 +0100] rev 57773
Metis is being used to emulate E steps;
src/HOL/TPTP/TPTP_Proof_Reconstruction.thy

2014-06-22 sultana [Sun, 22 Jun 2014 06:16:56 +0100] rev 57772
updated application of print_tac to take context parameter;
src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy

2014-08-02 blanchet [Sat, 02 Aug 2014 00:15:08 +0200] rev 57771
better duplicate detection
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

2014-08-01 blanchet [Fri, 01 Aug 2014 23:58:42 +0200] rev 57770
normalize conjectures vs. negated conjectures when comparing terms
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

2014-08-01 blanchet [Fri, 01 Aug 2014 23:33:43 +0200] rev 57769
tweaked 'clone' formula detection
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

2014-08-01 blanchet [Fri, 01 Aug 2014 23:29:50 +0200] rev 57768
fine-tuned Isar reconstruction, esp. boolean simplifications
src/HOL/Tools/ATP/atp_proof_reconstruct.ML src/HOL/Tools/SMT2/smtlib2_isar.ML src/HOL/Tools/SMT2/verit_isar.ML src/HOL/Tools/SMT2/z3_new_isar.ML src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML

2014-08-01 blanchet [Fri, 01 Aug 2014 23:29:49 +0200] rev 57767
centralized boolean simplification so that e.g. LEO-II benefits from it
src/HOL/Tools/ATP/atp_proof_reconstruct.ML src/HOL/Tools/SMT2/smtlib2_isar.ML src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

2014-08-01 blanchet [Fri, 01 Aug 2014 20:44:51 +0200] rev 57766
careful when compressing 'obtains'
src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML

2014-08-01 blanchet [Fri, 01 Aug 2014 20:44:29 +0200] rev 57765
better handling of variable names
src/HOL/Tools/ATP/atp_proof_reconstruct.ML src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML

2014-08-01 blanchet [Fri, 01 Aug 2014 20:15:41 +0200] rev 57764
try to get rid of skolems first
src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML