--- a/NEWS Sat Mar 05 19:58:56 2016 +0100
+++ b/NEWS Sat Mar 05 20:47:31 2016 +0100
@@ -23,6 +23,11 @@
*** HOL ***
+* New abbreviations for negated existence (but not bounded existence):
+
+ \<nexists>x. P x \<equiv> \<not> (\<exists>x. P x)
+ \<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x)
+
* The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@"
has been removed for output. It is retained for input only, until it is
eliminated altogether.
--- a/src/HOL/HOL.thy Sat Mar 05 19:58:56 2016 +0100
+++ b/src/HOL/HOL.thy Sat Mar 05 20:47:31 2016 +0100
@@ -105,6 +105,12 @@
subsubsection \<open>Additional concrete syntax\<close>
+abbreviation Not_Ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<nexists>" 10)
+ where "\<nexists>x. P x \<equiv> \<not> (\<exists>x. P x)"
+
+abbreviation Not_Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<nexists>!" 10)
+ where "\<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x)"
+
abbreviation not_equal :: "['a, 'a] \<Rightarrow> bool" (infixl "\<noteq>" 50)
where "x \<noteq> y \<equiv> \<not> (x = y)"
--- a/src/HOL/Library/LaTeXsugar.thy Sat Mar 05 19:58:56 2016 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy Sat Mar 05 20:47:31 2016 +0100
@@ -20,11 +20,6 @@
"_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 *)