NEWS
changeset 62522 d32c23d29968
parent 62521 6383440f41a8
child 62525 0c9081056829
--- a/NEWS	Sat Mar 05 19:58:56 2016 +0100
+++ b/NEWS	Sat Mar 05 20:47:31 2016 +0100
@@ -23,6 +23,11 @@
 
 *** HOL ***
 
+* New abbreviations for negated existence (but not bounded existence):
+
+  \<nexists>x. P x \<equiv> \<not> (\<exists>x. P x)
+  \<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x)
+
 * The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@"
 has been removed for output. It is retained for input only, until it is
 eliminated altogether.