[isabelle-dev] \nexists

[Makarius]

On 14/07/16 17:50, Lawrence Paulson wrote:

> What’s unfortunate is that the “negated exists” quantifier is available
> both for input and output in Isabelle, just not as a TeX macro.

The macro is available here (nipkow 2005-05-30):
http://isabelle.in.tum.de/repos/isabelle/annotate/d51a0a772094/lib/texinputs/isabellesym.sty#l224

It only needs the amssymb package.


	Makarius