| changeset 71924 | e5df9c8d9d4b |
| parent 71923 | 7b34a932eeb6 |
| child 71927 | ebcae4a19e78 |
--- a/NEWS Sat Jun 06 10:58:13 2020 +0200 +++ b/NEWS Mon Jun 08 15:09:57 2020 +0200 @@ -18,6 +18,9 @@ *** Pure *** +* Session Pure-Examples contains notable examples for Isabelle/Pure +(former entries of HOL-Isar_Examples). + * Definitions in locales produce rule which can be added as congruence rule to protect foundational terms during simplification.