# HG changeset patch
# User noschinl
# Date 1379418044 -7200
# Node ID 7e80b558c7513b57670ddf9f7305ef6a138c0003
# Parent  c5096c22892b7cff3d83c9548608583cfafc021c
NEWS: Simps_Case_Conv

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