Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
updated NEWS etc.
authorblanchet
Mon, 26 Nov 2012 11:46:19 +0100
changeset 50219 f6b95f0bba78
parent 50218 d50119e69453
child 50220 90280d85cd03
updated NEWS etc.
CONTRIBUTORS file | annotate | diff | comparison | revisions
NEWS file | annotate | diff | comparison | revisions 
--- 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.
 
--- 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
isabelle