[isabelle-dev] NEWS: HOL notation
makarius at sketis.net
Sat Mar 5 23:19:28 CET 2016
*** 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
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 ...
More information about the isabelle-dev