# HG changeset patch
# User lcp
# Date 753644903 -3600
# Node ID b0ec0c1bddb73ea474438bab6e3c38fd987b6cb8
# Parent  eec6bb9c58eada95bcfca052859a434a1b54b213
expandshort

diff -r eec6bb9c58ea -r b0ec0c1bddb7 src/ZF/ex/LListFn.ML
--- a/src/ZF/ex/LListFn.ML	Thu Nov 18 14:57:05 1993 +0100
+++ b/src/ZF/ex/LListFn.ML	Thu Nov 18 18:48:23 1993 +0100
@@ -43,7 +43,7 @@
 val flip_ss = ZF_ss addsimps [flip_LNil, flip_LCons, not_type];
 
 goal QUniv.thy "!!b. b:bool ==> b Int X : quniv(A)";
-be boolE 1;
+by (etac boolE 1);
 by (REPEAT (resolve_tac [one_Int_in_quniv, zero_Int_in_quniv] 1
      ORELSE etac ssubst 1));
 val bool_Int_into_quniv = result();
@@ -86,16 +86,16 @@
 val flip_llist_quniv_lemma = result();
 
 goal LListFn.thy "!!l. l: llist(bool) ==> flip(l) : quniv(bool)";
-br (flip_llist_quniv_lemma RS bspec RS Int_Vset_in_quniv) 1;
+by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_in_quniv) 1);
 by (REPEAT (assume_tac 1));
 val flip_in_quniv = result();
 
 val [prem] = goal LListFn.thy "l : llist(bool) ==> flip(l): llist(bool)";
 by (res_inst_tac [("X", "{flip(l) . l:llist(bool)}")]
        LList.coinduct 1);
-br (prem RS RepFunI) 1;
+by (rtac (prem RS RepFunI) 1);
 by (fast_tac (ZF_cs addSIs [flip_in_quniv]) 1);
-be RepFunE 1;
+by (etac RepFunE 1);
 by (etac LList.elim 1);
 by (asm_simp_tac flip_ss 1);
 by (asm_simp_tac flip_ss 1);
@@ -106,9 +106,9 @@
     "l : llist(bool) ==> flip(flip(l)) = l";
 by (res_inst_tac [("X1", "{<flip(flip(l)),l> . l:llist(bool)}")]
        (LList_Eq.coinduct RS lleq_implies_equal) 1);
-br (prem RS RepFunI) 1;
+by (rtac (prem RS RepFunI) 1);
 by (fast_tac (ZF_cs addSIs [flip_type]) 1);
-be RepFunE 1;
+by (etac RepFunE 1);
 by (etac LList.elim 1);
 by (asm_simp_tac flip_ss 1);
 by (asm_simp_tac (flip_ss addsimps [flip_type, not_not]) 1);
diff -r eec6bb9c58ea -r b0ec0c1bddb7 src/ZF/ex/Primrec0.ML
--- a/src/ZF/ex/Primrec0.ML	Thu Nov 18 14:57:05 1993 +0100
+++ b/src/ZF/ex/Primrec0.ML	Thu Nov 18 18:48:23 1993 +0100
@@ -337,7 +337,7 @@
 by (etac List.elim 1);
 by (asm_simp_tac (ack2_ss addsimps [[nat_le_refl, lt_ack2] MRS lt_trans]) 1);
 by (asm_simp_tac ack2_ss 1);
-be ssubst 1;  (*get rid of the needless assumption*)
+by (etac ssubst 1);  (*get rid of the needless assumption*)
 by (eres_inst_tac [("n","a")] nat_induct 1);
 (*base case*)
 by (DO_GOAL [asm_simp_tac ack2_ss, rtac lt_trans, etac bspec,
diff -r eec6bb9c58ea -r b0ec0c1bddb7 src/ZF/ex/llistfn.ML
--- a/src/ZF/ex/llistfn.ML	Thu Nov 18 14:57:05 1993 +0100
+++ b/src/ZF/ex/llistfn.ML	Thu Nov 18 18:48:23 1993 +0100
@@ -43,7 +43,7 @@
 val flip_ss = ZF_ss addsimps [flip_LNil, flip_LCons, not_type];
 
 goal QUniv.thy "!!b. b:bool ==> b Int X : quniv(A)";
-be boolE 1;
+by (etac boolE 1);
 by (REPEAT (resolve_tac [one_Int_in_quniv, zero_Int_in_quniv] 1
      ORELSE etac ssubst 1));
 val bool_Int_into_quniv = result();
@@ -86,16 +86,16 @@
 val flip_llist_quniv_lemma = result();
 
 goal LListFn.thy "!!l. l: llist(bool) ==> flip(l) : quniv(bool)";
-br (flip_llist_quniv_lemma RS bspec RS Int_Vset_in_quniv) 1;
+by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_in_quniv) 1);
 by (REPEAT (assume_tac 1));
 val flip_in_quniv = result();
 
 val [prem] = goal LListFn.thy "l : llist(bool) ==> flip(l): llist(bool)";
 by (res_inst_tac [("X", "{flip(l) . l:llist(bool)}")]
        LList.coinduct 1);
-br (prem RS RepFunI) 1;
+by (rtac (prem RS RepFunI) 1);
 by (fast_tac (ZF_cs addSIs [flip_in_quniv]) 1);
-be RepFunE 1;
+by (etac RepFunE 1);
 by (etac LList.elim 1);
 by (asm_simp_tac flip_ss 1);
 by (asm_simp_tac flip_ss 1);
@@ -106,9 +106,9 @@
     "l : llist(bool) ==> flip(flip(l)) = l";
 by (res_inst_tac [("X1", "{<flip(flip(l)),l> . l:llist(bool)}")]
        (LList_Eq.coinduct RS lleq_implies_equal) 1);
-br (prem RS RepFunI) 1;
+by (rtac (prem RS RepFunI) 1);
 by (fast_tac (ZF_cs addSIs [flip_type]) 1);
-be RepFunE 1;
+by (etac RepFunE 1);
 by (etac LList.elim 1);
 by (asm_simp_tac flip_ss 1);
 by (asm_simp_tac (flip_ss addsimps [flip_type, not_not]) 1);
diff -r eec6bb9c58ea -r b0ec0c1bddb7 src/ZF/ex/primrec0.ML
--- a/src/ZF/ex/primrec0.ML	Thu Nov 18 14:57:05 1993 +0100
+++ b/src/ZF/ex/primrec0.ML	Thu Nov 18 18:48:23 1993 +0100
@@ -337,7 +337,7 @@
 by (etac List.elim 1);
 by (asm_simp_tac (ack2_ss addsimps [[nat_le_refl, lt_ack2] MRS lt_trans]) 1);
 by (asm_simp_tac ack2_ss 1);
-be ssubst 1;  (*get rid of the needless assumption*)
+by (etac ssubst 1);  (*get rid of the needless assumption*)
 by (eres_inst_tac [("n","a")] nat_induct 1);
 (*base case*)
 by (DO_GOAL [asm_simp_tac ack2_ss, rtac lt_trans, etac bspec,