src/HOL/Induct/LList.ML
changeset 5184 9b8547a9496a
parent 5148 74919e8f221c
child 5278 a903b66822e2
     1.1 --- a/src/HOL/Induct/LList.ML	Fri Jul 24 13:03:20 1998 +0200
     1.2 +++ b/src/HOL/Induct/LList.ML	Fri Jul 24 13:19:38 1998 +0200
     1.3 @@ -155,10 +155,10 @@
     1.4  by (safe_tac ((claset_of Fun.thy) delrules [equalityI]));
     1.5  by (etac LListD.elim 1);
     1.6  by (safe_tac (claset_of Prod.thy delrules [equalityI] addSEs [diagE]));
     1.7 -by (res_inst_tac [("n", "n")] natE 1);
     1.8 +by (exhaust_tac "n" 1);
     1.9  by (Asm_simp_tac 1);
    1.10  by (rename_tac "n'" 1);
    1.11 -by (res_inst_tac [("n", "n'")] natE 1);
    1.12 +by (exhaust_tac "n'" 1);
    1.13  by (asm_simp_tac (simpset() addsimps [CONS_def]) 1);
    1.14  by (asm_simp_tac (simpset() addsimps [CONS_def, less_Suc_eq]) 1);
    1.15  qed "LListD_implies_ntrunc_equality";
    1.16 @@ -317,9 +317,9 @@
    1.17  by (stac prem2 1);
    1.18  by (Simp_tac 1);
    1.19  by (strip_tac 1);
    1.20 -by (res_inst_tac [("n", "n")] natE 1);
    1.21 +by (exhaust_tac "n" 1);
    1.22  by (rename_tac "m" 2);
    1.23 -by (res_inst_tac [("n", "m")] natE 2);
    1.24 +by (exhaust_tac "m" 2);
    1.25  by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
    1.26  result();
    1.27  
    1.28 @@ -782,12 +782,12 @@
    1.29  Goal
    1.30      "nat_rec (LCons b l) (%m. lmap(f)) n =      \
    1.31  \    LCons (nat_rec b (%m. f) n) (nat_rec l (%m. lmap(f)) n)";
    1.32 -by (nat_ind_tac "n" 1);
    1.33 +by (induct_tac "n" 1);
    1.34  by (ALLGOALS Asm_simp_tac);
    1.35  qed "fun_power_lmap";
    1.36  
    1.37  goal Nat.thy "nat_rec (g x) (%m. g) n = nat_rec x (%m. g) (Suc n)";
    1.38 -by (nat_ind_tac "n" 1);
    1.39 +by (induct_tac "n" 1);
    1.40  by (ALLGOALS Asm_simp_tac);
    1.41  qed "fun_power_Suc";
    1.42