src/ZF/ex/llistfn.ML
changeset 128 b0ec0c1bddb7
parent 120 09287f26bfb8
child 173 85071e6ad295
     1.1 --- a/src/ZF/ex/llistfn.ML	Thu Nov 18 14:57:05 1993 +0100
     1.2 +++ b/src/ZF/ex/llistfn.ML	Thu Nov 18 18:48:23 1993 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4  val flip_ss = ZF_ss addsimps [flip_LNil, flip_LCons, not_type];
     1.5  
     1.6  goal QUniv.thy "!!b. b:bool ==> b Int X : quniv(A)";
     1.7 -be boolE 1;
     1.8 +by (etac boolE 1);
     1.9  by (REPEAT (resolve_tac [one_Int_in_quniv, zero_Int_in_quniv] 1
    1.10       ORELSE etac ssubst 1));
    1.11  val bool_Int_into_quniv = result();
    1.12 @@ -86,16 +86,16 @@
    1.13  val flip_llist_quniv_lemma = result();
    1.14  
    1.15  goal LListFn.thy "!!l. l: llist(bool) ==> flip(l) : quniv(bool)";
    1.16 -br (flip_llist_quniv_lemma RS bspec RS Int_Vset_in_quniv) 1;
    1.17 +by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_in_quniv) 1);
    1.18  by (REPEAT (assume_tac 1));
    1.19  val flip_in_quniv = result();
    1.20  
    1.21  val [prem] = goal LListFn.thy "l : llist(bool) ==> flip(l): llist(bool)";
    1.22  by (res_inst_tac [("X", "{flip(l) . l:llist(bool)}")]
    1.23         LList.coinduct 1);
    1.24 -br (prem RS RepFunI) 1;
    1.25 +by (rtac (prem RS RepFunI) 1);
    1.26  by (fast_tac (ZF_cs addSIs [flip_in_quniv]) 1);
    1.27 -be RepFunE 1;
    1.28 +by (etac RepFunE 1);
    1.29  by (etac LList.elim 1);
    1.30  by (asm_simp_tac flip_ss 1);
    1.31  by (asm_simp_tac flip_ss 1);
    1.32 @@ -106,9 +106,9 @@
    1.33      "l : llist(bool) ==> flip(flip(l)) = l";
    1.34  by (res_inst_tac [("X1", "{<flip(flip(l)),l> . l:llist(bool)}")]
    1.35         (LList_Eq.coinduct RS lleq_implies_equal) 1);
    1.36 -br (prem RS RepFunI) 1;
    1.37 +by (rtac (prem RS RepFunI) 1);
    1.38  by (fast_tac (ZF_cs addSIs [flip_type]) 1);
    1.39 -be RepFunE 1;
    1.40 +by (etac RepFunE 1);
    1.41  by (etac LList.elim 1);
    1.42  by (asm_simp_tac flip_ss 1);
    1.43  by (asm_simp_tac (flip_ss addsimps [flip_type, not_not]) 1);