Changed succ(1) to 2 in in_VLimit, two_in_univ
authorlcp
Fri Dec 23 16:29:53 1994 +0100 (1994-12-23)
changeset 82803d7bfa70289
parent 827 aa332949ce1a
child 829 ba28811c3496
Changed succ(1) to 2 in in_VLimit, two_in_univ
src/ZF/Univ.ML
     1.1 --- a/src/ZF/Univ.ML	Fri Dec 23 16:29:04 1994 +0100
     1.2 +++ b/src/ZF/Univ.ML	Fri Dec 23 16:29:53 1994 +0100
     1.3 @@ -325,7 +325,7 @@
     1.4  (*Infer that a, b occur at ordinals x,xa < i.*)
     1.5  by (rtac ([aprem,limiti] MRS Limit_VfromE) 1);
     1.6  by (rtac ([bprem,limiti] MRS Limit_VfromE) 1);
     1.7 -by (res_inst_tac [("j1", "x Un xa Un succ(1)")] (step RS exE) 1);
     1.8 +by (res_inst_tac [("j1", "x Un xa Un 2")] (step RS exE) 1);
     1.9  by (DO_GOAL [etac conjE, etac Limit_VfromI, rtac limiti, atac] 5);
    1.10  by (etac (Vfrom_UnI2 RS Vfrom_UnI1) 4);
    1.11  by (etac (Vfrom_UnI1 RS Vfrom_UnI1) 3);
    1.12 @@ -451,7 +451,7 @@
    1.13  by (rtac (rank RS ssubst) 1);
    1.14  by (rtac equalityI 1);
    1.15  by (safe_tac ZF_cs);
    1.16 -by (EVERY' [wtac UN_I, 
    1.17 +by (EVERY' [rtac UN_I, 
    1.18  	    etac (i_subset_Vfrom RS subsetD),
    1.19  	    etac (Ord_in_Ord RS rank_of_Ord RS ssubst),
    1.20  	    assume_tac,
    1.21 @@ -591,7 +591,7 @@
    1.22  qed "one_in_univ";
    1.23  
    1.24  (*unused!*)
    1.25 -goal Univ.thy "succ(1) : univ(A)";
    1.26 +goal Univ.thy "2 : univ(A)";
    1.27  by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1));
    1.28  qed "two_in_univ";
    1.29