1.1 --- a/NEWS	Tue Sep 17 08:42:51 2013 +0200
     1.2 +++ b/NEWS	Tue Sep 17 13:40:44 2013 +0200
     1.3 @@ -238,6 +238,11 @@
     1.4  
     1.5    declare [[case_translation case_combinator constructor1 ... constructorN]]
     1.6  
     1.7 +* New Library/Simps_Case_Conv.thy: Provides commands simps_of_case and
     1.8 +case_of_simps to convert function definitions between a list of
     1.9 +equations with patterns on the lhs and a single equation with case
    1.10 +expressions on the rhs. See also Ex/Simps_Case_Conv_Examples.thy.
    1.11 +
    1.12  * Notation "{p:A. P}" now allows tuple patterns as well.
    1.13  
    1.14  * Revised devices for recursive definitions over finite sets: