[isabelle-dev] \nexists

[Johannes Hölzl]

Am Freitag, den 15.07.2016, 11:30 +0200 schrieb 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/te
> xinputs/isabellesym.sty#l224
> 
> It only needs the amssymb package.
> 

Added amssymb to HOL-MV_A. And reintroduced \nexists in ef794d2e3754.

 - Johannes