clarified notation: iterated quantifier is negated as one chunk;
authorwenzelm
Sun Sep 18 17:59:28 2016 +0200 (2016-09-18)
changeset 639129f8325206465
parent 63911 d00d4f399f05
child 63914 255294779d40
child 63915 bab633745c7f
clarified notation: iterated quantifier is negated as one chunk;
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Sun Sep 18 16:59:15 2016 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sun Sep 18 17:59:28 2016 +0200
     1.3 @@ -117,11 +117,13 @@
     1.4  \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
     1.5  
     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 +syntax
    1.10 +  "_Not_Ex" :: "idts \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<nexists>_./ _)" [0, 10] 10)
    1.11 +  "_Not_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<nexists>!_./ _)" [0, 10] 10)
    1.12 +translations
    1.13 +  "\<nexists>x. P" \<rightleftharpoons> "\<not> (\<exists>x. P)"
    1.14 +  "\<nexists>!x. P" \<rightleftharpoons> "\<not> (\<exists>!x. P)"
    1.15  
    1.16 -abbreviation Not_Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<nexists>!" 10)
    1.17 -  where "\<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x)"
    1.18  
    1.19  abbreviation not_equal :: "['a, 'a] \<Rightarrow> bool"  (infixl "\<noteq>" 50)
    1.20    where "x \<noteq> y \<equiv> \<not> (x = y)"