src/HOL/HOL.thy
changeset 62522 d32c23d29968
parent 62521 6383440f41a8
child 62913 13252110a6fe
     1.1 --- a/src/HOL/HOL.thy	Sat Mar 05 19:58:56 2016 +0100
     1.2 +++ b/src/HOL/HOL.thy	Sat Mar 05 20:47:31 2016 +0100
     1.3 @@ -105,6 +105,12 @@
     1.4  
     1.5  subsubsection \<open>Additional concrete syntax\<close>
     1.6  
     1.7 +abbreviation Not_Ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<nexists>" 10)
     1.8 +  where "\<nexists>x. P x \<equiv> \<not> (\<exists>x. P x)"
     1.9 +
    1.10 +abbreviation Not_Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<nexists>!" 10)
    1.11 +  where "\<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x)"
    1.12 +
    1.13  abbreviation not_equal :: "['a, 'a] \<Rightarrow> bool"  (infixl "\<noteq>" 50)
    1.14    where "x \<noteq> y \<equiv> \<not> (x = y)"
    1.15