NEWS and CONTRIBUTORS
authortraytel
Wed Apr 10 17:49:16 2013 +0200 (2013-04-10)
changeset 51682bdaa1582dc8b
parent 51681 bdfa3b947992
child 51683 baefa3b461c2
NEWS and CONTRIBUTORS
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Wed Apr 10 17:49:16 2013 +0200
     1.2 +++ b/CONTRIBUTORS	Wed Apr 10 17:49:16 2013 +0200
     1.3 @@ -6,6 +6,12 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* April 2013: Stefan Berghofer, secunet Security Networks AG
     1.8 +  Dmitriy Traytel, TUM
     1.9 +  Makarius Wenzel, Université Paris-Sud / LRI
    1.10 +  Case translations as a separate check phase independent of the
    1.11 +  datatype package.
    1.12 +
    1.13  * March 2013: Florian Haftmann, TUM
    1.14    Reform of "big operators" on sets.
    1.15  
     2.1 --- a/NEWS	Wed Apr 10 17:49:16 2013 +0200
     2.2 +++ b/NEWS	Wed Apr 10 17:49:16 2013 +0200
     2.3 @@ -43,6 +43,13 @@
     2.4  
     2.5  *** HOL ***
     2.6  
     2.7 +* Nested case expressions are now translated in a separate check
     2.8 +  phase rather than during parsing. The data for case combinators
     2.9 +  is separated from the datatype package. The declaration attribute
    2.10 +  "case_translation" can be used to register new case combinators:
    2.11 +
    2.12 +  declare [[case_translation case_combinator constructor1 ... constructorN]]
    2.13 +
    2.14  * Notation "{p:A. P}" now allows tuple patterns as well.
    2.15  
    2.16  * Revised devices for recursive definitions over finite sets: