[isabelle-dev] Notation for not-exists

[Makarius]

The Isabelle symbol \<nexists> has been there for many years, even with a 
standard abbreviation "~?" for the Prover IDE.

A comment in LaTeXsugar.thy from 2005 
http://isabelle.in.tum.de/repos/isabelle/file/922e702ae8ca/src/HOL/Library/LaTeXsugar.thy#l23 
says: (* should become standard syntax once x-symbols supports it *)

Proof General Emacs and the X-Symbol package no longer exist, and the 
terminology of "x-symbols" is long-forgotten, but we have proper means to 
introduce notation that works unconditionally in the Prover IDE and 
document output:

abbreviation Not_Ex :: "('a ⇒ bool) ⇒ bool"  (binder "∄" 10)
   where "∄x. P x ≡ ¬ (∃x. P x)"


Trying this with find_theorems in HOL Main or Library shows relatively few 
occurrences, so it is likely not to cause great confusion.

There is a conflict with old "HOL" print mode, though. It causes a mixture 
of "! " and "? " versus "∄" in output. I can't imagine anybody using that 
print mode seriously, so maybe it is time to make these syntax variants 
input-only, as a preparation for removal at a later point.


 	Makarius