2014-02-02 blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55254
'primitive' is not an adverb
src/Doc/Datatypes/Datatypes.thy

2014-02-02 blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55253
unform treatment of preplay_timeout = 0 and > 0
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML

2014-02-02 blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55252
refactor data structure (step 1)
src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML

2014-02-02 blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55251
tuned code
src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML

2014-02-02 blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55250
tuned factor
src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML

2014-02-02 blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55249
tuning
src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML

2014-02-02 blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55248
made SML/NJ happier
src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML

2014-02-02 blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55247
take intersection rather than union of methods when merging steps -- more efficient and natural
src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML

2014-02-02 blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55246
merge proof methods
src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML

2014-02-02 blanchet [Sun, 02 Feb 2014 20:53:51 +0100] rev 55245
use Skolem proof methods appropriately
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML