[isabelle-dev] \nexists

Makarius makarius at sketis.net
Fri Jul 15 11:30:22 CEST 2016

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):

It only needs the amssymb package.


More information about the isabelle-dev mailing list