equal
deleted
inserted
replaced
198 lemma (in reflection) Closed_Unbounded_ClEx: |
198 lemma (in reflection) Closed_Unbounded_ClEx: |
199 "(!!a. [| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) <-> Q(a,x)) |
199 "(!!a. [| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) <-> Q(a,x)) |
200 ==> Closed_Unbounded(ClEx(P))" |
200 ==> Closed_Unbounded(ClEx(P))" |
201 apply (unfold ClEx_eq FF_def F0_def M_def) |
201 apply (unfold ClEx_eq FF_def F0_def M_def) |
202 apply (rule ex_reflection.ZF_Closed_Unbounded_ClEx [of Mset _ _ Cl]) |
202 apply (rule ex_reflection.ZF_Closed_Unbounded_ClEx [of Mset _ _ Cl]) |
203 apply (rule ex_reflection.intro, assumption) |
203 apply (rule ex_reflection.intro, rule reflection_axioms) |
204 apply (blast intro: ex_reflection_axioms.intro) |
204 apply (blast intro: ex_reflection_axioms.intro) |
205 done |
205 done |
206 |
206 |
207 subsection{*Packaging the Quantifier Reflection Rules*} |
207 subsection{*Packaging the Quantifier Reflection Rules*} |
208 |
208 |