updated NEWS etc.
authorblanchet
Mon Nov 26 11:46:19 2012 +0100 (2012-11-26)
changeset 50219f6b95f0bba78
parent 50218 d50119e69453
child 50220 90280d85cd03
updated NEWS etc.
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Mon Nov 26 11:45:12 2012 +0100
     1.2 +++ b/CONTRIBUTORS	Mon Nov 26 11:46:19 2012 +0100
     1.3 @@ -9,6 +9,10 @@
     1.4  * 2012: Makarius Wenzel, Université Paris-Sud / LRI
     1.5    Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.
     1.6  
     1.7 +* Fall 2012: Steffen Smolka, TUM
     1.8 +  Various improvements to Sledgehammer's Isar proof generator, including
     1.9 +  a smart type annotation algorithm and proof shrinking.
    1.10 +
    1.11  * November 2012: Fabian Immler, TUM
    1.12    "Symbols" dockable for Isabelle/jEdit.
    1.13  
     2.1 --- a/NEWS	Mon Nov 26 11:45:12 2012 +0100
     2.2 +++ b/NEWS	Mon Nov 26 11:46:19 2012 +0100
     2.3 @@ -274,8 +274,9 @@
     2.4  
     2.5    - Added MaSh relevance filter based on machine-learning; see the
     2.6      Sledgehammer manual for details.
     2.7 +  - Polished Isar proofs generated with "isar_proofs" option.
     2.8    - Rationalized type encodings ("type_enc" option).
     2.9 -  - Renamed "kill_provers" subcommand to "kill"
    2.10 +  - Renamed "kill_provers" subcommand to "kill".
    2.11    - Renamed options:
    2.12        isar_proof ~> isar_proofs
    2.13        isar_shrink_factor ~> isar_shrink