| changeset 71788 | ca3ac5238c41 |
| parent 71753 | 65b7d9ec05f5 |
| child 71808 | e2ad50885887 |
--- a/NEWS Wed Apr 22 19:22:43 2020 +0200 +++ b/NEWS Tue Apr 21 07:28:17 2020 +0000 @@ -24,6 +24,11 @@ INCOMPATIBILITY. +*** Pure *** + +* Definitions in locales produce rule which can be added as congruence +rule to protect foundational terms during simplification. + New in Isabelle2020 (April 2020) --------------------------------