# HG changeset patch
# User paulson
# Date 903352180 -7200
# Node ID 8f9056ce5dfbd04ea1b175aa67376c215ab1c7d0
# Parent  f7a5e06adea1c09e649e07118eee8d84666dcf44
expandshort

diff -r f7a5e06adea1 -r 8f9056ce5dfb src/HOL/Lambda/InductTermi.ML
--- 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);
diff -r f7a5e06adea1 -r 8f9056ce5dfb src/HOL/Lambda/Lambda.ML
--- 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];
diff -r f7a5e06adea1 -r 8f9056ce5dfb src/HOL/Lambda/ListBeta.ML
--- 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);
diff -r f7a5e06adea1 -r 8f9056ce5dfb src/HOL/Lambda/ListOrder.ML
--- 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);