src/ZF/Constructible/Rec_Separation.thy
changeset 13505 52a16cb7fefb
parent 13503 d93f41fe35d2
child 13506 acc18a5d2b1a
     1.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Fri Aug 16 12:48:49 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Fri Aug 16 16:41:48 2002 +0200
     1.3 @@ -82,7 +82,7 @@
     1.4  lemma rtrancl_separation:
     1.5       "[| L(r); L(A) |] ==> separation (L, rtran_closure_mem(L,A,r))"
     1.6  apply (rule separation_CollectI)
     1.7 -apply (rule_tac A="{r,A,z}" in subset_LsetE, blast )
     1.8 +apply (rule_tac A="{r,A,z}" in subset_LsetE, blast)
     1.9  apply (rule ReflectsE [OF rtran_closure_mem_reflection], assumption)
    1.10  apply (drule subset_Lset_ltD, assumption)
    1.11  apply (erule reflection_imp_L_separation)
    1.12 @@ -190,7 +190,7 @@
    1.13                \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
    1.14                 w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp)"
    1.15  apply (rule separation_CollectI)
    1.16 -apply (rule_tac A="{r,Z,z}" in subset_LsetE, blast )
    1.17 +apply (rule_tac A="{r,Z,z}" in subset_LsetE, blast)
    1.18  apply (rule ReflectsE [OF wellfounded_trancl_reflects], assumption)
    1.19  apply (drule subset_Lset_ltD, assumption)
    1.20  apply (erule reflection_imp_L_separation)
    1.21 @@ -252,7 +252,7 @@
    1.22        separation (L, \<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
    1.23           ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))"
    1.24  apply (rule separation_CollectI)
    1.25 -apply (rule_tac A="{r,z}" in subset_LsetE, blast )
    1.26 +apply (rule_tac A="{r,z}" in subset_LsetE, blast)
    1.27  apply (rule ReflectsE [OF wfrank_Reflects], assumption)
    1.28  apply (drule subset_Lset_ltD, assumption)
    1.29  apply (erule reflection_imp_L_separation)
    1.30 @@ -294,7 +294,7 @@
    1.31  apply (rule rallI)
    1.32  apply (rename_tac B)
    1.33  apply (rule separation_CollectI)
    1.34 -apply (rule_tac A="{B,r,z}" in subset_LsetE, blast )
    1.35 +apply (rule_tac A="{B,r,z}" in subset_LsetE, blast)
    1.36  apply (rule ReflectsE [OF wfrank_replacement_Reflects], assumption)
    1.37  apply (drule subset_Lset_ltD, assumption)
    1.38  apply (erule reflection_imp_L_separation)
    1.39 @@ -333,7 +333,7 @@
    1.40               M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
    1.41               ordinal(L,rangef)))"
    1.42  apply (rule separation_CollectI)
    1.43 -apply (rule_tac A="{r,z}" in subset_LsetE, blast )
    1.44 +apply (rule_tac A="{r,z}" in subset_LsetE, blast)
    1.45  apply (rule ReflectsE [OF Ord_wfrank_Reflects], assumption)
    1.46  apply (drule subset_Lset_ltD, assumption)
    1.47  apply (erule reflection_imp_L_separation)
    1.48 @@ -411,7 +411,7 @@
    1.49  apply (rule separation_CollectI)
    1.50  apply (insert nonempty)
    1.51  apply (subgoal_tac "L(Memrel(succ(n)))")
    1.52 -apply (rule_tac A="{B,A,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast )
    1.53 +apply (rule_tac A="{B,A,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast)
    1.54  apply (rule ReflectsE [OF list_replacement1_Reflects], assumption)
    1.55  apply (drule subset_Lset_ltD, assumption)
    1.56  apply (erule reflection_imp_L_separation)
    1.57 @@ -492,7 +492,7 @@
    1.58  apply (rule separation_CollectI)
    1.59  apply (insert nonempty)
    1.60  apply (subgoal_tac "L(Memrel(succ(n)))")
    1.61 -apply (rule_tac A="{B,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast )
    1.62 +apply (rule_tac A="{B,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast)
    1.63  apply (rule ReflectsE [OF formula_replacement1_Reflects], assumption)
    1.64  apply (drule subset_Lset_ltD, assumption)
    1.65  apply (erule reflection_imp_L_separation)
    1.66 @@ -612,7 +612,7 @@
    1.67  apply (rule rallI)
    1.68  apply (rule separation_CollectI)
    1.69  apply (subgoal_tac "L(Memrel(succ(n)))")
    1.70 -apply (rule_tac A="{A,n,w,z,Memrel(succ(n))}" in subset_LsetE, blast )
    1.71 +apply (rule_tac A="{A,n,w,z,Memrel(succ(n))}" in subset_LsetE, blast)
    1.72  apply (rule ReflectsE [OF nth_replacement_Reflects], assumption)
    1.73  apply (drule subset_Lset_ltD, assumption)
    1.74  apply (erule reflection_imp_L_separation)
    1.75 @@ -680,7 +680,7 @@
    1.76  apply (rename_tac B)
    1.77  apply (rule separation_CollectI)
    1.78  apply (subgoal_tac "L(Memrel(succ(n)))")
    1.79 -apply (rule_tac A="{B,A,n,z,Memrel(succ(n))}" in subset_LsetE, blast )
    1.80 +apply (rule_tac A="{B,A,n,z,Memrel(succ(n))}" in subset_LsetE, blast)
    1.81  apply (rule ReflectsE [OF eclose_replacement1_Reflects], assumption)
    1.82  apply (drule subset_Lset_ltD, assumption)
    1.83  apply (erule reflection_imp_L_separation)