# HG changeset patch
# User blanchet
# Date 1353926779 -3600
# Node ID f6b95f0bba785410df52ebcda54c19a853fed502
# Parent  d50119e694534f868827a9553d4b34788c5ef331
updated NEWS etc.

diff -r d50119e69453 -r f6b95f0bba78 CONTRIBUTORS
--- a/CONTRIBUTORS	Mon Nov 26 11:45:12 2012 +0100
+++ b/CONTRIBUTORS	Mon Nov 26 11:46:19 2012 +0100
@@ -9,6 +9,10 @@
 * 2012: Makarius Wenzel, Université Paris-Sud / LRI
   Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.
 
+* Fall 2012: Steffen Smolka, TUM
+  Various improvements to Sledgehammer's Isar proof generator, including
+  a smart type annotation algorithm and proof shrinking.
+
 * November 2012: Fabian Immler, TUM
   "Symbols" dockable for Isabelle/jEdit.
 
diff -r d50119e69453 -r f6b95f0bba78 NEWS
--- a/NEWS	Mon Nov 26 11:45:12 2012 +0100
+++ b/NEWS	Mon Nov 26 11:46:19 2012 +0100
@@ -274,8 +274,9 @@
 
   - Added MaSh relevance filter based on machine-learning; see the
     Sledgehammer manual for details.
+  - Polished Isar proofs generated with "isar_proofs" option.
   - Rationalized type encodings ("type_enc" option).
-  - Renamed "kill_provers" subcommand to "kill"
+  - Renamed "kill_provers" subcommand to "kill".
   - Renamed options:
       isar_proof ~> isar_proofs
       isar_shrink_factor ~> isar_shrink