*** 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_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
