changeset 71927 | ebcae4a19e78 |
parent 71924 | e5df9c8d9d4b |
child 71932 | 65fd0f032a75 |
--- a/NEWS Mon Jun 08 21:55:14 2020 +0200 +++ b/NEWS Mon Jun 08 21:56:06 2020 +0200 @@ -27,6 +27,9 @@ *** HOL *** +* Session HOL-Examples contains notable examples for Isabelle/HOL +(former entries of HOL-Isar_Examples, HOL-ex etc.). + * 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).