--- 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}}
--- 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 *)