--- a/src/HOL/Lambda/InductTermi.ML Mon Aug 17 13:09:08 1998 +0200
+++ b/src/HOL/Lambda/InductTermi.ML Mon Aug 17 13:09:40 1998 +0200
@@ -26,7 +26,7 @@
qed_spec_mp "double_induction_lemma";
Goal "t : IT ==> t : termi(beta)";
-be IT.induct 1;
+by (etac IT.induct 1);
by (dtac rev_subsetD 1);
by (rtac lists_mono 1);
by (rtac Int_lower2 1);
@@ -95,7 +95,7 @@
by (res_inst_tac [("t","r")] Apps_dB_induct 1);
by (rename_tac "n ts" 1);
by (Clarify_tac 1);
- brs IT.intrs 1;
+ by (resolve_tac IT.intrs 1);
by (Clarify_tac 1);
by (EVERY1[dtac bspec, atac]);
by (etac mp 1);
@@ -113,7 +113,7 @@
by (rename_tac "s ss" 1);
by (Asm_full_simp_tac 1);
by (Clarify_tac 1);
-brs IT.intrs 1;
+by (resolve_tac IT.intrs 1);
by (blast_tac (claset() addIs [apps_preserves_beta]) 1);
by (etac mp 1);
by (Clarify_tac 1);
--- a/src/HOL/Lambda/Lambda.ML Mon Aug 17 13:09:08 1998 +0200
+++ b/src/HOL/Lambda/Lambda.ML Mon Aug 17 13:09:40 1998 +0200
@@ -139,13 +139,13 @@
(* Not used in CR-proof but in SN-proof *)
Goal "r -> s ==> !t i. r[t/i] -> s[t/i]";
-be beta.induct 1;
+by (etac beta.induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [subst_subst RS sym])));
qed_spec_mp "subst_preserves_beta";
Addsimps [subst_preserves_beta];
Goal "r -> s ==> !i. lift r i -> lift s i";
-be beta.induct 1;
+by (etac beta.induct 1);
by (Auto_tac);
qed_spec_mp "lift_preserves_beta";
Addsimps [lift_preserves_beta];
--- a/src/HOL/Lambda/ListBeta.ML Mon Aug 17 13:09:08 1998 +0200
+++ b/src/HOL/Lambda/ListBeta.ML Mon Aug 17 13:09:40 1998 +0200
@@ -6,7 +6,7 @@
Goal
"v -> v' ==> !rs. v = (Var n)$$rs --> (? ss. rs => ss & v' = (Var n)$$ss)";
-be beta.induct 1;
+by (etac beta.induct 1);
by (Asm_full_simp_tac 1);
by (rtac allI 1);
by (res_inst_tac [("xs","rs")] rev_exhaust 1);
@@ -28,7 +28,7 @@
\ ( (? r'. r -> r' & u' = r'$$rs) | \
\ (? rs'. rs => rs' & u' = r$$rs') | \
\ (? s t ts. r = Abs s & rs = t#ts & u' = s[t/0]$$ts))";
-be beta.induct 1;
+by (etac beta.induct 1);
by (clarify_tac (claset() delrules [disjCI]) 1);
by (exhaust_tac "r" 1);
by (Asm_full_simp_tac 1);
--- a/src/HOL/Lambda/ListOrder.ML Mon Aug 17 13:09:08 1998 +0200
+++ b/src/HOL/Lambda/ListOrder.ML Mon Aug 17 13:09:40 1998 +0200
@@ -83,7 +83,7 @@
AddSIs [Cons_acc_step1I];
Goal "xs : lists(acc r) ==> xs : acc(step1 r)";
-be lists.induct 1;
+by (etac lists.induct 1);
by (rtac accI 1);
by (asm_full_simp_tac (simpset() addsimps [step1_def]) 1);
by (rtac accI 1);