[isabelle-dev] NEWS: HOL notation

[Makarius]

*** HOL ***

* New abbreviations for negated existence (but not bounded existence):

   ∄x. P x ≡ ¬ (∃x. P x)
   ∄!x. P x ≡ ¬ (∃!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.


This refers to Isabelle/6383440f41a8 and Isabelle/d32c23d29968.

Bounded existence refers to:

"∄x∈A. P x"
"∄x⊆A. P x"
"∄x⊂A. P x"

I did not touch this for now, since it is a bit entangled due to still 
existing plain ASCII variants. There is always something left open ...


 	Makarius