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