NEWS
changeset 71836 c095d3143047
parent 71834 919a55257e62
child 71837 dca11678c495
--- 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