equal
deleted
inserted
replaced
154 by blast |
154 by blast |
155 |
155 |
156 lemma "{x. P x \<longrightarrow> Q x} = -{x. P x} \<union> {x. Q x}" |
156 lemma "{x. P x \<longrightarrow> Q x} = -{x. P x} \<union> {x. Q x}" |
157 by blast |
157 by blast |
158 |
158 |
159 constdefs |
159 definition prime :: "nat set" where |
160 prime :: "nat set" |
|
161 "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}" |
160 "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}" |
162 |
161 |
163 lemma "{p*q | p q. p\<in>prime \<and> q\<in>prime} = |
162 lemma "{p*q | p q. p\<in>prime \<and> q\<in>prime} = |
164 {z. \<exists>p q. z = p*q \<and> p\<in>prime \<and> q\<in>prime}" |
163 {z. \<exists>p q. z = p*q \<and> p\<in>prime \<and> q\<in>prime}" |
165 by (rule refl) |
164 by (rule refl) |