# HG changeset patch
# User nipkow
# Date 1117434118 -7200
# Node ID c423bb89186def1ef06dfab6002ab058345d50a7
# Parent  e8c169d6f1915d6b4808ad888648ee3f889c0903
added \nexists

diff -r e8c169d6f191 -r c423bb89186d lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Sun May 29 12:41:40 2005 +0200
+++ b/lib/texinputs/isabellesym.sty	Mon May 30 08:21:58 2005 +0200
@@ -220,6 +220,7 @@
 \newcommand{\isasymOr}{\isamath{\bigvee}}
 \newcommand{\isasymforall}{\isamath{\forall\,}}
 \newcommand{\isasymexists}{\isamath{\exists\,}}
+\newcommand{\isasymnexists}{\isamath{\nexists\,}}  %requires amssymb
 \newcommand{\isasymbox}{\isamath{\Box}}  %requires amssymb
 \newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires amssymb
 \newcommand{\isasymturnstile}{\isamath{\vdash}}
diff -r e8c169d6f191 -r c423bb89186d src/HOL/Library/LaTeXsugar.thy
--- a/src/HOL/Library/LaTeXsugar.thy	Sun May 29 12:41:40 2005 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy	Mon May 30 08:21:58 2005 +0200
@@ -20,6 +20,12 @@
   "_case_syntax":: "['a, cases_syn] => 'b"
   ("(\<^raw:\textsf{>case\<^raw:}> _ \<^raw:\textsf{>of\<^raw:}>/ _)" 10)
 
+(* should become standard syntax once x-symbols supports it *)
+syntax (latex)
+  nexists :: "('a => bool) => bool"           (binder "\<nexists>" 10)
+translations
+  "\<nexists>x. P" <= "\<not>(\<exists>x. P)"
+
 (* SETS *)
 
 (* empty set *)