changeset 69569 2d88bf80c84f
parent 69546 27dae626822b
parent 69568 de09a7261120
child 69580 6f755e3cd95d
--- a/NEWS	Tue Jan 01 13:26:37 2019 +0100
+++ b/NEWS	Tue Jan 01 18:33:19 2019 +0100
@@ -92,6 +92,13 @@
 * SMT: reconstruction is now possible using the SMT solver veriT.
+* HOL-Library.Simps_Case_Conv: case_of_simps now supports overlapping 
+and non-exhaustive patterns and handles arbitrarily nested patterns.
+It uses on the same algorithm as HOL-Library.Code_Lazy, which assumes
+sequential left-to-right pattern matching. The generated
+equation no longer tuples the arguments on the right-hand side.
 * Session HOL-SPARK: .prv files are no longer written to the
 file-system, but exported to the session database. Results may be
 retrieved with the "isabelle export" command-line tool like this: