[isabelle-dev] Notation for not-exists

[Tobias Nipkow]

On 04/03/2016 12:34, Makarius wrote:
> 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 *)

I wrote that comment and am still in favour.

Tobias

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5132 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160304/a223d287/attachment.bin>