2014-06-29 blanchet [Sun, 29 Jun 2014 21:07:53 +0200] rev 57436
removed non-existing MaSh component from list
etc/components

2014-06-29 haftmann [Sun, 29 Jun 2014 18:02:18 +0200] rev 57435
modernized diagnostic options
src/Tools/Code/code_runtime.ML src/Tools/nbe.ML

2014-06-29 blanchet [Sun, 29 Jun 2014 18:30:24 +0200] rev 57434
use SMT2
src/HOL/ROOT src/HOL/TPTP/MaSh_Eval.thy src/HOL/TPTP/mash_eval.ML

2014-06-29 blanchet [Sun, 29 Jun 2014 18:28:27 +0200] rev 57433
compile
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML

2014-06-29 blanchet [Sun, 29 Jun 2014 18:28:27 +0200] rev 57432
tuning
src/HOL/TPTP/mash_eval.ML src/HOL/TPTP/mash_export.ML src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

2014-06-29 blanchet [Sun, 29 Jun 2014 18:28:27 +0200] rev 57431
killed Python version of MaSh, now that the SML version works adequately
NEWS src/Doc/Sledgehammer/document/root.tex src/HOL/TPTP/MaSh_Export.thy src/HOL/TPTP/mash_eval.ML src/HOL/TPTP/mash_export.ML src/HOL/Tools/Sledgehammer/MaSh/etc/settings src/HOL/Tools/Sledgehammer/MaSh/src/ExpandFeatures.py src/HOL/Tools/Sledgehammer/MaSh/src/KNN.py src/HOL/Tools/Sledgehammer/MaSh/src/KNNs.py src/HOL/Tools/Sledgehammer/MaSh/src/argparse.py src/HOL/Tools/Sledgehammer/MaSh/src/compareStats.py src/HOL/Tools/Sledgehammer/MaSh/src/dictionaries.py src/HOL/Tools/Sledgehammer/MaSh/src/mash.py src/HOL/Tools/Sledgehammer/MaSh/src/parameters.py src/HOL/Tools/Sledgehammer/MaSh/src/predefined.py src/HOL/Tools/Sledgehammer/MaSh/src/readData.py src/HOL/Tools/Sledgehammer/MaSh/src/server.py src/HOL/Tools/Sledgehammer/MaSh/src/singleNaiveBayes.py src/HOL/Tools/Sledgehammer/MaSh/src/snow.py src/HOL/Tools/Sledgehammer/MaSh/src/sparseNaiveBayes.py src/HOL/Tools/Sledgehammer/MaSh/src/spawnDaemon.py src/HOL/Tools/Sledgehammer/MaSh/src/stats.py src/HOL/Tools/Sledgehammer/MaSh/src/tester.py src/HOL/Tools/Sledgehammer/MaSh/src/theoryModels.py src/HOL/Tools/Sledgehammer/MaSh/src/theoryStats.py src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML src/HOL/Tools/etc/options

2014-06-28 haftmann [Sat, 28 Jun 2014 22:13:23 +0200] rev 57430
tracing facilities for the code generator preprocessor
NEWS src/Pure/Isar/code.ML src/Tools/Code/code_preproc.ML src/Tools/Code_Generator.thy

2014-06-28 haftmann [Sat, 28 Jun 2014 22:13:21 +0200] rev 57429
tuned interface
src/Pure/Isar/code.ML src/Tools/Code/code_preproc.ML

2014-06-28 haftmann [Sat, 28 Jun 2014 22:13:20 +0200] rev 57428
corrected handled exception
src/Tools/Code/code_namespace.ML

2014-06-28 haftmann [Sat, 28 Jun 2014 21:09:17 +0200] rev 57427
proper trading of variables;
more appropriate ML variable names
src/HOL/Library/Code_Abstract_Nat.thy