equal
deleted
inserted
replaced
271 by blast |
271 by blast |
272 |
272 |
273 lemma rex_is_bex [simp]: "(\<exists>x[%z. z\<in>A]. P(x)) <-> (\<exists>x\<in>A. P(x))" |
273 lemma rex_is_bex [simp]: "(\<exists>x[%z. z\<in>A]. P(x)) <-> (\<exists>x\<in>A. P(x))" |
274 by blast |
274 by blast |
275 |
275 |
276 lemma atomize_rall: "(!!x. M(x) ==> P(x)) == Trueprop (\<forall>x[M]. P(x))"; |
276 lemma atomize_rall: "(!!x. M(x) ==> P(x)) == Trueprop (\<forall>x[M]. P(x))" |
277 by (simp add: rall_def atomize_all atomize_imp) |
277 by (simp add: rall_def atomize_all atomize_imp) |
278 |
278 |
279 declare atomize_rall [symmetric, rulify] |
279 declare atomize_rall [symmetric, rulify] |
280 |
280 |
281 lemma rall_simps1: |
281 lemma rall_simps1: |