1.1 --- a/src/HOL/Lambda/InductTermi.ML	Mon Aug 17 13:09:08 1998 +0200
     1.2 +++ b/src/HOL/Lambda/InductTermi.ML	Mon Aug 17 13:09:40 1998 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  qed_spec_mp "double_induction_lemma";
     1.5  
     1.6  Goal "t : IT ==> t : termi(beta)";
     1.7 -be IT.induct 1;
     1.8 +by (etac IT.induct 1);
     1.9    by (dtac rev_subsetD 1);
    1.10     by (rtac lists_mono 1);
    1.11     by (rtac Int_lower2 1);
    1.12 @@ -95,7 +95,7 @@
    1.13  by (res_inst_tac [("t","r")] Apps_dB_induct 1);
    1.14   by (rename_tac "n ts" 1);
    1.15   by (Clarify_tac 1);
    1.16 - brs IT.intrs 1;
    1.17 + by (resolve_tac IT.intrs 1);
    1.18   by (Clarify_tac 1);
    1.19   by (EVERY1[dtac bspec, atac]);
    1.20   by (etac mp 1);
    1.21 @@ -113,7 +113,7 @@
    1.22  by (rename_tac "s ss" 1);
    1.23  by (Asm_full_simp_tac 1);
    1.24  by (Clarify_tac 1);
    1.25 -brs IT.intrs 1;
    1.26 +by (resolve_tac IT.intrs 1);
    1.27   by (blast_tac (claset() addIs [apps_preserves_beta]) 1);
    1.28  by (etac mp 1);
    1.29   by (Clarify_tac 1);

     2.1 --- a/src/HOL/Lambda/Lambda.ML	Mon Aug 17 13:09:08 1998 +0200
     2.2 +++ b/src/HOL/Lambda/Lambda.ML	Mon Aug 17 13:09:40 1998 +0200
     2.3 @@ -139,13 +139,13 @@
     2.4  (* Not used in CR-proof but in SN-proof *)
     2.5  
     2.6  Goal "r -> s ==> !t i. r[t/i] -> s[t/i]";
     2.7 -be beta.induct 1;
     2.8 +by (etac beta.induct 1);
     2.9  by (ALLGOALS (asm_simp_tac (simpset() addsimps [subst_subst RS sym])));
    2.10  qed_spec_mp "subst_preserves_beta";
    2.11  Addsimps [subst_preserves_beta];
    2.12  
    2.13  Goal "r -> s ==> !i. lift r i -> lift s i";
    2.14 -be beta.induct 1;
    2.15 +by (etac beta.induct 1);
    2.16  by (Auto_tac);
    2.17  qed_spec_mp "lift_preserves_beta";
    2.18  Addsimps [lift_preserves_beta];

     3.1 --- a/src/HOL/Lambda/ListBeta.ML	Mon Aug 17 13:09:08 1998 +0200
     3.2 +++ b/src/HOL/Lambda/ListBeta.ML	Mon Aug 17 13:09:40 1998 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  
     3.5  Goal
     3.6   "v -> v' ==> !rs. v = (Var n)$$rs --> (? ss. rs => ss & v' = (Var n)$$ss)";
     3.7 -be beta.induct 1;
     3.8 +by (etac beta.induct 1);
     3.9  by (Asm_full_simp_tac 1);
    3.10  by (rtac allI 1);
    3.11  by (res_inst_tac [("xs","rs")] rev_exhaust 1);
    3.12 @@ -28,7 +28,7 @@
    3.13  \     ( (? r'. r -> r' & u' = r'$$rs) | \
    3.14  \       (? rs'. rs => rs' & u' = r$$rs') | \
    3.15  \       (? s t ts. r = Abs s & rs = t#ts & u' = s[t/0]$$ts))";
    3.16 -be beta.induct 1;
    3.17 +by (etac beta.induct 1);
    3.18     by (clarify_tac (claset() delrules [disjCI]) 1);
    3.19     by (exhaust_tac "r" 1);
    3.20       by (Asm_full_simp_tac 1);

     4.1 --- a/src/HOL/Lambda/ListOrder.ML	Mon Aug 17 13:09:08 1998 +0200
     4.2 +++ b/src/HOL/Lambda/ListOrder.ML	Mon Aug 17 13:09:40 1998 +0200
     4.3 @@ -83,7 +83,7 @@
     4.4  AddSIs [Cons_acc_step1I];
     4.5  
     4.6  Goal "xs : lists(acc r) ==> xs : acc(step1 r)";
     4.7 -be lists.induct 1;
     4.8 +by (etac lists.induct 1);
     4.9   by (rtac accI 1);
    4.10   by (asm_full_simp_tac (simpset() addsimps [step1_def]) 1);
    4.11  by (rtac accI 1);