Isabelle allows you to use symbols that are negated versions of certain other symbols. Examples are ≠
and ∉
. Is there a mechanism for getting negated versions of arbitrary symbols, like the \not
macro in LaTeX?
Your question has two parts: whether arbitrary negated symbols can be used, and whether such symbols can be input with a convenient macro. Let's start with the first part:
The Isabelle FAQ explains that JEdit converts mathematical symbols input in various ways to Unicode, and uses/displays the unicode symbol. Therefore, if your desired symbol exists in Unicode, there is a chance that you could use it directly (i.e. ctrl-c ctrl-v the symbol). For example, the following allows you to define "not exists":
abbreviation notexists :: "(('a ⇒ bool) ⇒ bool)" ("∄") where "∄ Φ ≡ (¬ (∃x. Φ(x)))"
However, not all unicode symbols are available. For instance, the italic nabla does not display correctly in jedit.
Now to the second part of your question: as far as I know, such a macro doesn't exist. However, Isabelle has a similar macro mechanism for making symbols boldface. For example, \<bold> \<exists>
will be displayed as a bold "exists" symbol. This shows that the macro functionality exists, and it could be possible to have a macro for negating symbols, as you suggested, in the future.