equal
deleted
inserted
replaced
102 definition Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<exists>!" 10) |
102 definition Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<exists>!" 10) |
103 where "Ex1 P \<equiv> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x)" |
103 where "Ex1 P \<equiv> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x)" |
104 |
104 |
105 |
105 |
106 subsubsection \<open>Additional concrete syntax\<close> |
106 subsubsection \<open>Additional concrete syntax\<close> |
|
107 |
|
108 abbreviation Not_Ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<nexists>" 10) |
|
109 where "\<nexists>x. P x \<equiv> \<not> (\<exists>x. P x)" |
|
110 |
|
111 abbreviation Not_Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<nexists>!" 10) |
|
112 where "\<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x)" |
107 |
113 |
108 abbreviation not_equal :: "['a, 'a] \<Rightarrow> bool" (infixl "\<noteq>" 50) |
114 abbreviation not_equal :: "['a, 'a] \<Rightarrow> bool" (infixl "\<noteq>" 50) |
109 where "x \<noteq> y \<equiv> \<not> (x = y)" |
115 where "x \<noteq> y \<equiv> \<not> (x = y)" |
110 |
116 |
111 notation (output) |
117 notation (output) |