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.