--- a/NEWS Tue May 12 16:53:13 2020 +0100
+++ b/NEWS Mon May 04 17:35:29 2020 +0200
@@ -451,6 +451,10 @@
*** HOL ***
+* Simproc 'datatype_no_proper_subterm' rewrites equalities 'lhs = rhs'
+on datatypes to 'False' if either side is a proper subexpression of the
+other (for any datatype with a reasonable size function).
+
* Command 'export_code' produces output as logical files within the
theory context, as well as formal session exports that can be
materialized via command-line tools "isabelle export" or "isabelle build