| changeset 71834 | 919a55257e62 |
| parent 71808 | e2ad50885887 |
| child 71836 | c095d3143047 |
--- a/NEWS Tue May 12 15:11:20 2020 +0100 +++ b/NEWS Tue May 12 16:53:02 2020 +0100 @@ -33,6 +33,11 @@ * Definitions in locales produce rule which can be added as congruence rule to protect foundational terms during simplification. +*** HOL *** + +* Added the "at most 1" quantifier, Uniq. + +* For the natural numbers, Sup{} = 0. New in Isabelle2020 (April 2020) --------------------------------