introduced induct_thm_tac
authornipkow
Wed Aug 30 16:29:21 2000 +0200 (2000-08-30)
changeset 9747043098ba5098
parent 9746 64b803edef39
child 9748 67486cf2f8f6
introduced induct_thm_tac
src/HOL/IMP/Transition.ML
src/HOL/Induct/LList.ML
src/HOL/Induct/Multiset.ML
src/HOL/Induct/Perm.ML
src/HOL/Induct/SList.ML
src/HOL/Integ/IntDiv.ML
src/HOL/Integ/int_arith2.ML
src/HOL/Lambda/ListApplication.ML
src/HOL/Lambda/ListBeta.ML
src/HOL/Lambda/ParRed.ML
src/HOL/Lex/MaxChop.ML
src/HOL/Lex/Prefix.ML
src/HOL/Lex/RegExp2NAe.ML
src/HOL/List.ML
src/HOL/MiniML/MiniML.ML
src/HOL/MiniML/Type.ML
src/HOL/NumberTheory/EulerFermat.ML
src/HOL/NumberTheory/IntFact.ML
src/HOL/NumberTheory/IntPrimes.ML
src/HOL/NumberTheory/WilsonRuss.ML
src/HOL/Real/Hyperreal/Zorn.ML
src/HOL/Real/PNat.ML
src/HOL/Real/PReal.ML
src/HOL/Subst/AList.ML
src/HOL/Tools/datatype_package.ML
src/HOL/UNITY/AllocBase.ML
src/HOL/UNITY/GenPrefix.ML
src/HOL/While.ML
src/HOL/ex/Factorization.ML
src/HOL/ex/Fib.ML
src/HOL/ex/Primes.ML
src/HOL/ex/Primrec.ML
src/HOL/ex/Puzzle.ML
src/HOL/ex/Qsort.ML
src/HOL/ex/Recdefs.ML
     1.1 --- a/src/HOL/IMP/Transition.ML	Wed Aug 30 16:24:29 2000 +0200
     1.2 +++ b/src/HOL/IMP/Transition.ML	Wed Aug 30 16:29:21 2000 +0200
     1.3 @@ -93,7 +93,7 @@
     1.4  (* WHILE, induction on the length of the computation *)
     1.5  by (eres_inst_tac [("P","?X -n-> ?Y")] rev_mp 1);
     1.6  by (res_inst_tac [("x","s")] spec 1);
     1.7 -by (res_inst_tac [("n","n")] less_induct 1);
     1.8 +by (induct_thm_tac less_induct "n" 1);
     1.9  by (strip_tac 1);
    1.10  by (etac rel_pow_E2 1);
    1.11   by (Asm_full_simp_tac 1);
    1.12 @@ -214,7 +214,7 @@
    1.13  qed_spec_mp "comp_decomp_lemma";
    1.14  
    1.15  Goal "!c s t. (c,s) -n-> (SKIP,t) --> <c,s> -c-> t";
    1.16 -by (res_inst_tac [("n","n")] less_induct 1);
    1.17 +by (induct_thm_tac less_induct "n" 1);
    1.18  by (Clarify_tac 1);
    1.19  by (etac rel_pow_E2 1);
    1.20   by (asm_full_simp_tac (simpset() addsimps evalc.intrs) 1);
     2.1 --- a/src/HOL/Induct/LList.ML	Wed Aug 30 16:24:29 2000 +0200
     2.2 +++ b/src/HOL/Induct/LList.ML	Wed Aug 30 16:29:21 2000 +0200
     2.3 @@ -128,7 +128,7 @@
     2.4  qed "LListD_unfold";
     2.5  
     2.6  Goal "!M N. (M,N) : LListD(diag A) --> ntrunc k M = ntrunc k N";
     2.7 -by (res_inst_tac [("n", "k")] less_induct 1);
     2.8 +by (induct_thm_tac less_induct "k" 1);
     2.9  by (safe_tac (claset() delrules [equalityI]));
    2.10  by (etac LListD.elim 1);
    2.11  by (safe_tac (claset() delrules [equalityI]));
    2.12 @@ -287,7 +287,7 @@
    2.13  by (rtac (ntrunc_equality RS ext) 1);
    2.14  by (rename_tac "x k" 1);
    2.15  by (res_inst_tac [("x", "x")] spec 1);
    2.16 -by (res_inst_tac [("n", "k")] less_induct 1);
    2.17 +by (induct_thm_tac less_induct "k" 1);
    2.18  by (rename_tac "n" 1);
    2.19  by (rtac allI 1);
    2.20  by (rename_tac "y" 1);
     3.1 --- a/src/HOL/Induct/Multiset.ML	Wed Aug 30 16:24:29 2000 +0200
     3.2 +++ b/src/HOL/Induct/Multiset.ML	Wed Aug 30 16:29:21 2000 +0200
     3.3 @@ -457,7 +457,7 @@
     3.4  by (Clarify_tac 1);
     3.5  by (rotate_tac ~1 1);
     3.6  by (etac rev_mp 1);
     3.7 -by (res_inst_tac [("M","K")] multiset_induct 1);
     3.8 +by (induct_thm_tac multiset_induct "K" 1);
     3.9   by (Asm_simp_tac 1);
    3.10  by (simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
    3.11  by (Blast_tac 1);
    3.12 @@ -476,7 +476,7 @@
    3.13  qed "lemma3";
    3.14  
    3.15  Goalw [W_def] "wf(r) ==> M : W";
    3.16 -by (res_inst_tac [("M","M")] multiset_induct 1);
    3.17 +by (induct_thm_tac multiset_induct "M" 1);
    3.18   by (rtac accI 1);
    3.19   by (Asm_full_simp_tac 1);
    3.20  by (blast_tac (claset() addDs [export lemma3]) 1);
     4.1 --- a/src/HOL/Induct/Perm.ML	Wed Aug 30 16:24:29 2000 +0200
     4.2 +++ b/src/HOL/Induct/Perm.ML	Wed Aug 30 16:29:21 2000 +0200
     4.3 @@ -145,7 +145,7 @@
     4.4  AddIffs [cons_perm_eq];
     4.5  
     4.6  Goal "ALL xs ys. zs@xs <~~> zs@ys --> xs <~~> ys";
     4.7 -by (res_inst_tac [("xs","zs")] rev_induct 1);
     4.8 +by (rev_induct_tac "zs" 1);
     4.9  by (ALLGOALS Full_simp_tac);
    4.10  by (Blast_tac 1);
    4.11  qed_spec_mp "append_perm_imp_perm";
     5.1 --- a/src/HOL/Induct/SList.ML	Wed Aug 30 16:24:29 2000 +0200
     5.2 +++ b/src/HOL/Induct/SList.ML	Wed Aug 30 16:29:21 2000 +0200
     5.3 @@ -52,7 +52,7 @@
     5.4  
     5.5  (*Perform induction on xs. *)
     5.6  fun list_ind_tac a M = 
     5.7 -    EVERY [res_inst_tac [("l",a)] list_induct2 M,
     5.8 +    EVERY [induct_thm_tac list_induct2 a M,
     5.9             rename_last_tac a ["1"] (M+1)];
    5.10  
    5.11  (*** Isomorphisms ***)
     6.1 --- a/src/HOL/Integ/IntDiv.ML	Wed Aug 30 16:24:29 2000 +0200
     6.2 +++ b/src/HOL/Integ/IntDiv.ML	Wed Aug 30 16:29:21 2000 +0200
     6.3 @@ -113,7 +113,7 @@
     6.4  
     6.5  (*Correctness of posDivAlg: it computes quotients correctly*)
     6.6  Goal "#0 <= a --> #0 < b --> quorem ((a, b), posDivAlg (a, b))";
     6.7 -by (res_inst_tac [("u", "a"), ("v", "b")] posDivAlg_induct 1);
     6.8 +by (induct_thm_tac posDivAlg_induct "a b" 1);
     6.9  by Auto_tac;
    6.10  by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def])));
    6.11  (*base case: a<b*)
    6.12 @@ -152,7 +152,7 @@
    6.13  (*Correctness of negDivAlg: it computes quotients correctly
    6.14    It doesn't work if a=0 because the 0/b=0 rather than -1*)
    6.15  Goal "a < #0 --> #0 < b --> quorem ((a, b), negDivAlg (a, b))";
    6.16 -by (res_inst_tac [("u", "a"), ("v", "b")] negDivAlg_induct 1);
    6.17 +by (induct_thm_tac negDivAlg_induct "a b" 1);
    6.18  by Auto_tac;
    6.19  by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def])));
    6.20  (*base case: 0<=a+b*)
     7.1 --- a/src/HOL/Integ/int_arith2.ML	Wed Aug 30 16:24:29 2000 +0200
     7.2 +++ b/src/HOL/Integ/int_arith2.ML	Wed Aug 30 16:29:21 2000 +0200
     7.3 @@ -88,7 +88,7 @@
     7.4  
     7.5  (*Analogous to zadd_int, but more easily provable using the arithmetic in Bin*)
     7.6  Goal "n<=m --> int m - int n = int (m-n)";
     7.7 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
     7.8 +by (induct_thm_tac diff_induct "m n" 1);
     7.9  by Auto_tac;
    7.10  qed_spec_mp "zdiff_int";
    7.11  
     8.1 --- a/src/HOL/Lambda/ListApplication.ML	Wed Aug 30 16:24:29 2000 +0200
     8.2 +++ b/src/HOL/Lambda/ListApplication.ML	Wed Aug 30 16:29:21 2000 +0200
     8.3 @@ -97,7 +97,7 @@
     8.4  "[| !!n ts. !t : set ts. P t ==> P((Var n)$$ts); \
     8.5  \   !!u ts. [| P u; !t : set ts. P t |] ==> P((Abs u)$$ts) \
     8.6  \|] ==> !t. size t = n --> P t";
     8.7 -by (res_inst_tac [("n","n")] less_induct 1);
     8.8 +by (induct_thm_tac less_induct "n" 1);
     8.9  by (rtac allI 1);
    8.10  by (cut_inst_tac [("t","t")] ex_head_tail 1);
    8.11  by (Clarify_tac 1);
     9.1 --- a/src/HOL/Lambda/ListBeta.ML	Wed Aug 30 16:24:29 2000 +0200
     9.2 +++ b/src/HOL/Lambda/ListBeta.ML	Wed Aug 30 16:29:21 2000 +0200
     9.3 @@ -66,7 +66,7 @@
     9.4  AddSEs [apps_betasE];
     9.5  
     9.6  Goal "r -> s ==> r$$ss -> s$$ss";
     9.7 -by (res_inst_tac [("xs","ss")] rev_induct 1);
     9.8 +by (rev_induct_tac "ss" 1);
     9.9  by (Auto_tac);
    9.10  qed "apps_preserves_beta";
    9.11  Addsimps [apps_preserves_beta];
    9.12 @@ -79,7 +79,7 @@
    9.13  Addsimps [apps_preserves_beta2];
    9.14  
    9.15  Goal "!ss. rs => ss --> r$$rs -> r$$ss";
    9.16 -by (res_inst_tac [("xs","rs")] rev_induct 1);
    9.17 +by (rev_induct_tac "rs" 1);
    9.18   by (Asm_full_simp_tac 1);
    9.19  by (Asm_full_simp_tac 1);
    9.20  by (Clarify_tac 1);
    10.1 --- a/src/HOL/Lambda/ParRed.ML	Wed Aug 30 16:24:29 2000 +0200
    10.2 +++ b/src/HOL/Lambda/ParRed.ML	Wed Aug 30 16:29:21 2000 +0200
    10.3 @@ -83,7 +83,7 @@
    10.4  (*** cd ***)
    10.5  
    10.6  Goal "!t. s => t --> t => cd s";
    10.7 -by (res_inst_tac[("x","s")] cd.induct 1);
    10.8 +by (induct_thm_tac cd.induct "s" 1);
    10.9  by (Auto_tac);
   10.10  by (fast_tac (claset() addSIs [par_beta_subst]) 1);
   10.11  qed_spec_mp "par_beta_cd";
    11.1 --- a/src/HOL/Lex/MaxChop.ML	Wed Aug 30 16:24:29 2000 +0200
    11.2 +++ b/src/HOL/Lex/MaxChop.ML	Wed Aug 30 16:29:21 2000 +0200
    11.3 @@ -33,7 +33,7 @@
    11.4  
    11.5  Goal "is_maxsplitter P splitf ==> \
    11.6  \ !yss zs. chop splitf xs = (yss,zs) --> xs = concat yss @ zs";
    11.7 -by (res_inst_tac [("xs","xs")] length_induct 1);
    11.8 +by (induct_thm_tac length_induct "xs" 1);
    11.9  by (asm_simp_tac (simpset() delsplits [split_if]
   11.10                             addsimps [chop_rule,is_maxsplitter_reducing]) 1);
   11.11  by (asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
   11.12 @@ -42,7 +42,7 @@
   11.13  
   11.14  Goal "is_maxsplitter P splitf ==> \
   11.15  \ !yss zs. chop splitf xs = (yss,zs) --> (!ys : set yss. ys ~= [])";
   11.16 -by (res_inst_tac [("xs","xs")] length_induct 1);
   11.17 +by (induct_thm_tac length_induct "xs" 1);
   11.18  by (asm_simp_tac (simpset() addsimps [chop_rule,is_maxsplitter_reducing]) 1);
   11.19  by (asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
   11.20                                   addsplits [split_split]) 1);
    12.1 --- a/src/HOL/Lex/Prefix.ML	Wed Aug 30 16:24:29 2000 +0200
    12.2 +++ b/src/HOL/Lex/Prefix.ML	Wed Aug 30 16:29:21 2000 +0200
    12.3 @@ -81,7 +81,7 @@
    12.4  qed "prefix_Cons";
    12.5  
    12.6  Goal "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))";
    12.7 -by (res_inst_tac [("xs","zs")] rev_induct 1);
    12.8 +by (rev_induct_tac "zs" 1);
    12.9   by (Force_tac 1);
   12.10  by (asm_full_simp_tac (simpset() delsimps [append_assoc]
   12.11                                   addsimps [append_assoc RS sym])1);
    13.1 --- a/src/HOL/Lex/RegExp2NAe.ML	Wed Aug 30 16:24:29 2000 +0200
    13.2 +++ b/src/HOL/Lex/RegExp2NAe.ML	Wed Aug 30 16:29:21 2000 +0200
    13.3 @@ -500,7 +500,7 @@
    13.4  \ (? us v. w = concat us @ v & \
    13.5  \             (!u:set us. accepts A u) & \
    13.6  \             (? r. (start A,r) : steps A v & rr = True#r))";
    13.7 -by (res_inst_tac [("xs","w")] rev_induct 1);
    13.8 +by (rev_induct_tac "w" 1);
    13.9   by (Asm_full_simp_tac 1);
   13.10   by (Clarify_tac 1);
   13.11   by (res_inst_tac [("x","[]")] exI 1);
    14.1 --- a/src/HOL/List.ML	Wed Aug 30 16:24:29 2000 +0200
    14.2 +++ b/src/HOL/List.ML	Wed Aug 30 16:29:21 2000 +0200
    14.3 @@ -414,10 +414,10 @@
    14.4  by (eresolve_tac prems 1);
    14.5  qed "rev_induct";
    14.6  
    14.7 -fun rev_induct_tac xs = res_inst_tac [("xs",xs)] rev_induct;
    14.8 +val rev_induct_tac = induct_thm_tac rev_induct;
    14.9  
   14.10  Goal  "(xs = [] --> P) -->  (!ys y. xs = ys@[y] --> P) --> P";
   14.11 -by (res_inst_tac [("xs","xs")] rev_induct 1);
   14.12 +by (rev_induct_tac "xs" 1);
   14.13  by Auto_tac;
   14.14  bind_thm ("rev_exhaust",
   14.15    impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp)))));
   14.16 @@ -752,7 +752,7 @@
   14.17  Addsimps [butlast_snoc];
   14.18  
   14.19  Goal "length(butlast xs) = length xs - 1";
   14.20 -by (res_inst_tac [("xs","xs")] rev_induct 1);
   14.21 +by (rev_induct_tac "xs" 1);
   14.22  by Auto_tac;
   14.23  qed "length_butlast";
   14.24  Addsimps [length_butlast];
   14.25 @@ -1217,7 +1217,7 @@
   14.26  qed "map_Suc_upt";
   14.27  
   14.28  Goal "ALL i. i < n-m --> (map f [m..n(]) ! i = f(m+i)";
   14.29 -by (res_inst_tac [("m","n"),("n","m")] diff_induct 1);
   14.30 +by (induct_thm_tac diff_induct "n m" 1);
   14.31  by (stac (map_Suc_upt RS sym) 3);
   14.32  by (auto_tac (claset(), simpset() addsimps [less_diff_conv, nth_upt]));
   14.33  qed_spec_mp "nth_map_upt";
   14.34 @@ -1453,14 +1453,14 @@
   14.35  
   14.36  Goal "map fst [p:zip xs [i..i + length xs(] . snd p : A] =     \
   14.37  \     map fst [p:zip xs [0..length xs(] . snd p + i : A]";
   14.38 -by (res_inst_tac [("xs","xs")] rev_induct 1);
   14.39 +by (rev_induct_tac "xs" 1);
   14.40   by (asm_simp_tac (simpset() addsimps [add_commute]) 2);
   14.41  by (Simp_tac 1);
   14.42  qed "sublist_shift_lemma";
   14.43  
   14.44  Goalw [sublist_def]
   14.45       "sublist (l@l') A = sublist l A @ sublist l' {j. j + length l : A}";
   14.46 -by (res_inst_tac [("xs","l'")] rev_induct 1);
   14.47 +by (rev_induct_tac "l'" 1);
   14.48  by (Simp_tac 1);
   14.49  by (asm_simp_tac (simpset() addsimps [inst "i" "0" upt_add_eq_append, 
   14.50  	                              zip_append, sublist_shift_lemma]) 1);
   14.51 @@ -1470,7 +1470,7 @@
   14.52  Addsimps [sublist_empty, sublist_nil];
   14.53  
   14.54  Goal "sublist (x#l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}";
   14.55 -by (res_inst_tac [("xs","l")] rev_induct 1);
   14.56 +by (rev_induct_tac "l" 1);
   14.57   by (asm_simp_tac (simpset() delsimps [append_Cons]
   14.58  	 		     addsimps [append_Cons RS sym, sublist_append]) 2);
   14.59  by (simp_tac (simpset() addsimps [sublist_def]) 1);
   14.60 @@ -1482,7 +1482,7 @@
   14.61  Addsimps [sublist_singleton];
   14.62  
   14.63  Goal "sublist l {..n(} = take n l";
   14.64 -by (res_inst_tac [("xs","l")] rev_induct 1);
   14.65 +by (rev_induct_tac "l" 1);
   14.66   by (asm_simp_tac (simpset() addsplits [nat_diff_split]
   14.67                               addsimps [sublist_append]) 2);
   14.68  by (Simp_tac 1);
    15.1 --- a/src/HOL/MiniML/MiniML.ML	Wed Aug 30 16:24:29 2000 +0200
    15.2 +++ b/src/HOL/MiniML/MiniML.ML	Wed Aug 30 16:29:21 2000 +0200
    15.3 @@ -114,7 +114,7 @@
    15.4  qed "free_tv_alpha";
    15.5  
    15.6  Goal "!!(k::nat). n <= n + k";
    15.7 -by (res_inst_tac [("n","k")] nat_induct 1);
    15.8 +by (induct_thm_tac nat_induct "k" 1);
    15.9  by (Simp_tac 1);
   15.10  by (Asm_simp_tac 1);
   15.11  val aux_plus = result();
    16.1 --- a/src/HOL/MiniML/Type.ML	Wed Aug 30 16:24:29 2000 +0200
    16.2 +++ b/src/HOL/MiniML/Type.ML	Wed Aug 30 16:29:21 2000 +0200
    16.3 @@ -150,7 +150,7 @@
    16.4  by (induct_tac "A" 1);
    16.5  by (Asm_full_simp_tac 1);
    16.6  by (rtac allI 1);
    16.7 -by (res_inst_tac [("n","n")] nat_induct 1);
    16.8 +by (induct_thm_tac nat_induct "n" 1);
    16.9  by (Asm_full_simp_tac 1);
   16.10  by (Asm_full_simp_tac 1);
   16.11  qed_spec_mp "free_tv_nth_A_impl_free_tv_A";
   16.12 @@ -161,7 +161,7 @@
   16.13  by (induct_tac "A" 1);
   16.14  by (Asm_full_simp_tac 1);
   16.15  by (rtac allI 1);
   16.16 -by (res_inst_tac [("n","nat")] nat_induct 1);
   16.17 +by (induct_thm_tac nat_induct "nat" 1);
   16.18  by (strip_tac 1);
   16.19  by (Asm_full_simp_tac 1);
   16.20  by (Simp_tac 1);
   16.21 @@ -505,7 +505,7 @@
   16.22  by (induct_tac "A" 1);
   16.23  by (Asm_full_simp_tac 1);
   16.24  by (rtac allI 1);
   16.25 -by (res_inst_tac [("n","nat")] nat_induct 1);
   16.26 +by (induct_thm_tac nat_induct "nat" 1);
   16.27  by (strip_tac 1);
   16.28  by (Asm_full_simp_tac 1);
   16.29  by (Simp_tac 1);
   16.30 @@ -718,7 +718,7 @@
   16.31  by (Asm_full_simp_tac 1);
   16.32  by (rtac allI 1);
   16.33  by (rename_tac "n1" 1);
   16.34 -by (res_inst_tac[("n","n1")] nat_induct 1);
   16.35 +by (induct_thm_tac nat_induct "n1" 1);
   16.36  by (Asm_full_simp_tac 1);
   16.37  by (Asm_full_simp_tac 1);
   16.38  qed_spec_mp "nth_subst";
    17.1 --- a/src/HOL/NumberTheory/EulerFermat.ML	Wed Aug 30 16:24:29 2000 +0200
    17.2 +++ b/src/HOL/NumberTheory/EulerFermat.ML	Wed Aug 30 16:29:21 2000 +0200
    17.3 @@ -30,7 +30,7 @@
    17.4  qed "BnorRset_induct";
    17.5  
    17.6  Goal "b:BnorRset(a,m) --> b<=a";
    17.7 -by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
    17.8 +by (induct_thm_tac BnorRset_induct "a m" 1);
    17.9  by (stac BnorRset_eq 2);
   17.10  by (rewtac Let_def);
   17.11  by Auto_tac;
   17.12 @@ -43,14 +43,14 @@
   17.13  qed "Bnor_mem_zle_swap";
   17.14  
   17.15  Goal "b:BnorRset(a,m) --> #0<b";
   17.16 -by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
   17.17 +by (induct_thm_tac BnorRset_induct "a m" 1);
   17.18  by (stac BnorRset_eq 2);
   17.19  by (rewtac Let_def);
   17.20  by Auto_tac;
   17.21  qed_spec_mp "Bnor_mem_zg"; 
   17.22  
   17.23  Goal "zgcd(b,m) = #1 --> #0<b --> b<=a --> b:BnorRset(a,m)";
   17.24 -by (res_inst_tac [("u","a"),("v","m")] BnorRset.induct 1);
   17.25 +by (induct_thm_tac BnorRset.induct "a m" 1);
   17.26  by Auto_tac;
   17.27  by (case_tac "a=b" 1);
   17.28  by (asm_full_simp_tac (simpset() addsimps [zle_neq_implies_zless]) 2);
   17.29 @@ -61,7 +61,7 @@
   17.30  qed_spec_mp "Bnor_mem_if";
   17.31  
   17.32  Goal "a<m --> BnorRset (a,m) : RsetR m";
   17.33 -by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
   17.34 +by (induct_thm_tac BnorRset_induct "a m" 1);
   17.35  by (Simp_tac 1);
   17.36  by (stac BnorRset_eq 1);
   17.37  by (rewtac Let_def);
   17.38 @@ -77,7 +77,7 @@
   17.39  qed_spec_mp "Bnor_in_RsetR";
   17.40  
   17.41  Goal "finite (BnorRset (a,m))";
   17.42 -by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
   17.43 +by (induct_thm_tac BnorRset_induct "a m" 1);
   17.44  by (stac BnorRset_eq 2);
   17.45  by (rewtac Let_def);
   17.46  by Auto_tac;
   17.47 @@ -210,7 +210,7 @@
   17.48  
   17.49  Goal "x~=#0 ==> a<m --> setprod ((%a. a*x) `` BnorRset(a,m)) = \
   17.50  \     setprod (BnorRset(a,m)) * x^card(BnorRset(a,m))";
   17.51 -by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
   17.52 +by (induct_thm_tac BnorRset_induct "a m" 1);
   17.53  by (stac BnorRset_eq 2);
   17.54  by (rewtac Let_def);
   17.55  by Auto_tac;
   17.56 @@ -235,7 +235,7 @@
   17.57  
   17.58  Goalw [norRRset_def,phi_def]
   17.59        "#0<m --> a<m --> zgcd (setprod (BnorRset (a,m)),m) = #1";
   17.60 -by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
   17.61 +by (induct_thm_tac BnorRset_induct "a m" 1);
   17.62  by (stac BnorRset_eq 2);
   17.63  by (rewtac Let_def);
   17.64  by Auto_tac;
   17.65 @@ -270,7 +270,7 @@
   17.66  Goalw [zprime_def] 
   17.67        "p:zprime ==> a<p --> (ALL b. #0<b & b<=a --> zgcd(b,p) = #1) \
   17.68  \      --> card (BnorRset(a, p)) = nat a";
   17.69 -by (res_inst_tac [("u","a"),("v","p")] BnorRset.induct 1);
   17.70 +by (induct_thm_tac BnorRset.induct "a p" 1);
   17.71  by (stac BnorRset_eq 1);
   17.72  by (rewtac Let_def);
   17.73  by Auto_tac;
    18.1 --- a/src/HOL/NumberTheory/IntFact.ML	Wed Aug 30 16:24:29 2000 +0200
    18.2 +++ b/src/HOL/NumberTheory/IntFact.ML	Wed Aug 30 16:29:21 2000 +0200
    18.3 @@ -42,13 +42,13 @@
    18.4  qed "d22set_induct";
    18.5  
    18.6  Goal "b:(d22set a) --> #1<b";
    18.7 -by (res_inst_tac [("u","a")] d22set_induct 1);
    18.8 +by (induct_thm_tac d22set_induct "a" 1);
    18.9  by (stac d22set_eq 2);
   18.10  by Auto_tac;
   18.11  qed_spec_mp "d22set_g_1";
   18.12  
   18.13  Goal "b:(d22set a) --> b<=a";
   18.14 -by (res_inst_tac [("u","a")] d22set_induct 1);
   18.15 +by (induct_thm_tac d22set_induct "a" 1);
   18.16  by (stac d22set_eq 2);
   18.17  by Auto_tac;
   18.18  qed_spec_mp "d22set_le";
   18.19 @@ -60,13 +60,13 @@
   18.20  qed "d22set_le_swap";
   18.21  
   18.22  Goal "#1<b --> b<=a --> b:(d22set a)";
   18.23 -by (res_inst_tac [("x","a")] d22set.induct 1);
   18.24 +by (induct_thm_tac d22set.induct "a" 1);
   18.25  by Auto_tac;
   18.26  by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [d22set_eq])));
   18.27  qed_spec_mp "d22set_mem";
   18.28  
   18.29  Goal "finite (d22set a)";
   18.30 -by (res_inst_tac [("u","a")] d22set_induct 1);
   18.31 +by (induct_thm_tac d22set_induct "a" 1);
   18.32  by (stac d22set_eq 2);
   18.33  by Auto_tac;
   18.34  qed "d22set_fin";
   18.35 @@ -75,7 +75,7 @@
   18.36  Delsimps zfact.simps; 
   18.37  
   18.38  Goal "setprod(d22set a) = zfact a";
   18.39 -by (res_inst_tac [("x","a")] d22set.induct 1);
   18.40 +by (induct_thm_tac d22set.induct "a" 1);
   18.41  by Safe_tac;
   18.42  by (asm_full_simp_tac (simpset() addsimps [d22set_eq,zfact_eq]) 1);
   18.43  by (stac d22set_eq 1);
    19.1 --- a/src/HOL/NumberTheory/IntPrimes.ML	Wed Aug 30 16:24:29 2000 +0200
    19.2 +++ b/src/HOL/NumberTheory/IntPrimes.ML	Wed Aug 30 16:29:21 2000 +0200
    19.3 @@ -181,7 +181,7 @@
    19.4  Addsimps [zgcd_0_1_iff];
    19.5  
    19.6  Goal "#0<=(n::int) --> (zgcd(m,n) dvd m) & (zgcd(m,n) dvd n)";
    19.7 -by (res_inst_tac [("u","m"),("v","n")] zgcd.induct 1);
    19.8 +by (induct_thm_tac zgcd.induct "m n" 1);
    19.9  by (case_tac "n=#0" 1);
   19.10  by (auto_tac (claset() addDs [zdvd_zmod_imp_zdvd],
   19.11                simpset() addsimps [zle_neq_implies_zless,neq_commute,
   19.12 @@ -198,14 +198,14 @@
   19.13  val lemma_false = result();
   19.14  
   19.15  Goal "#0<=(n::int) --> (f dvd m) --> (f dvd n) --> f dvd zgcd(m,n)";
   19.16 -by (res_inst_tac [("u","m"),("v","n")] zgcd.induct 1);
   19.17 +by (induct_thm_tac zgcd.induct "m n" 1);
   19.18  by (case_tac "n=#0" 1);
   19.19  by (auto_tac (claset() addDs [lemma_false] addIs [pos_mod_sign,zdvd_zmod],
   19.20          simpset() addsimps [zgcd_non_0,neq_commute,zle_neq_implies_zless]));
   19.21  qed_spec_mp "zgcd_greatest";
   19.22  
   19.23  Goal "#0 < (n::int) --> #0 < zgcd (m, n)";
   19.24 -by (res_inst_tac [("u","m"),("v","n")] zgcd.induct 1);
   19.25 +by (induct_thm_tac zgcd.induct "m n" 1);
   19.26  by (auto_tac (claset(), simpset() addsimps zgcd.simps));
   19.27  qed_spec_mp "zgcd_zless";
   19.28  
   19.29 @@ -269,7 +269,7 @@
   19.30  qed "zgcd_assoc";
   19.31  
   19.32  Goal "#0<=(n::int) --> #0<=k --> k * zgcd(m,n) = zgcd(k*m, k*n)";
   19.33 -by (res_inst_tac [("u","m"),("v","n")] zgcd.induct 1);
   19.34 +by (induct_thm_tac zgcd.induct "m n" 1);
   19.35  by (case_tac "n=#0" 1);
   19.36  by (auto_tac (claset() addDs [lemma_false],
   19.37                simpset() addsimps [zle_neq_implies_zless,pos_mod_sign,
    20.1 --- a/src/HOL/NumberTheory/WilsonRuss.ML	Wed Aug 30 16:24:29 2000 +0200
    20.2 +++ b/src/HOL/NumberTheory/WilsonRuss.ML	Wed Aug 30 16:29:21 2000 +0200
    20.3 @@ -175,7 +175,7 @@
    20.4  qed "wset_subset";
    20.5  
    20.6  Goal "p:zprime --> a<p-#1 --> b:(wset(a,p)) --> #1<b";
    20.7 -by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
    20.8 +by (induct_thm_tac wset_induct "a p" 1);
    20.9  by Auto_tac;
   20.10  by (case_tac "b=a" 1);
   20.11  by (case_tac "b=inv p a" 2);
   20.12 @@ -187,7 +187,7 @@
   20.13  qed_spec_mp "wset_g_1";
   20.14  
   20.15  Goal "p:zprime --> a<p-#1 --> b:(wset(a,p)) --> b<p-#1";
   20.16 -by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
   20.17 +by (induct_thm_tac wset_induct "a p" 1);
   20.18  by Auto_tac;
   20.19  by (case_tac "b=a" 1);
   20.20  by (case_tac "b=inv p a" 2);
   20.21 @@ -199,7 +199,7 @@
   20.22  qed_spec_mp "wset_less";
   20.23  
   20.24  Goal "p:zprime --> a<p-#1 --> #1<b --> b<=a --> b:(wset(a,p))"; 
   20.25 -by (res_inst_tac [("u","a"),("v","p")] wset.induct 1);
   20.26 +by (induct_thm_tac wset.induct "a p" 1);
   20.27  by Auto_tac;
   20.28  by (subgoal_tac "b=a" 1);
   20.29  by (rtac zle_anti_sym 2);
   20.30 @@ -210,7 +210,7 @@
   20.31  
   20.32  Goal "p:zprime --> #5<=p --> a<p-#1 --> b:(wset (a,p)) \
   20.33  \     --> (inv p b):(wset (a,p))";
   20.34 -by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
   20.35 +by (induct_thm_tac wset_induct "a p" 1);
   20.36  by Auto_tac;
   20.37  by (case_tac "b=a" 1);
   20.38  by (stac wset_eq 1);
   20.39 @@ -234,14 +234,14 @@
   20.40  qed "wset_inv_mem_mem";
   20.41  
   20.42  Goal "finite (wset (a,p))";
   20.43 -by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
   20.44 +by (induct_thm_tac wset_induct "a p" 1);
   20.45  by (stac wset_eq 2);
   20.46  by (rewtac Let_def);
   20.47  by Auto_tac;
   20.48  qed "wset_fin";
   20.49  
   20.50  Goal "p:zprime --> #5<=p --> a<p-#1 --> [setprod (wset (a,p)) = #1](mod p)";
   20.51 -by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
   20.52 +by (induct_thm_tac wset_induct "a p" 1);
   20.53  by (stac wset_eq 2);
   20.54  by (rewtac Let_def);
   20.55  by Auto_tac;
    21.1 --- a/src/HOL/Real/Hyperreal/Zorn.ML	Wed Aug 30 16:24:29 2000 +0200
    21.2 +++ b/src/HOL/Real/Hyperreal/Zorn.ML	Wed Aug 30 16:29:21 2000 +0200
    21.3 @@ -53,7 +53,7 @@
    21.4  
    21.5  (*Perform induction on n, then prove the major premise using prems. *)
    21.6  fun TFin_ind_tac a prems i = 
    21.7 -    EVERY [res_inst_tac [("n",a)] TFin_induct i,
    21.8 +    EVERY [induct_thm_tac TFin_induct a i,
    21.9             rename_last_tac a ["1"] (i+1),
   21.10             rename_last_tac a ["2"] (i+2),
   21.11             ares_tac prems i];
    22.1 --- a/src/HOL/Real/PNat.ML	Wed Aug 30 16:24:29 2000 +0200
    22.2 +++ b/src/HOL/Real/PNat.ML	Wed Aug 30 16:29:21 2000 +0200
    22.3 @@ -48,7 +48,7 @@
    22.4  
    22.5  (*Perform induction on n. *)
    22.6  fun pnat_ind_tac a i = 
    22.7 -  res_inst_tac [("n",a)] pnat_induct i  THEN  rename_last_tac a [""] (i+1);
    22.8 +  induct_thm_tac pnat_induct a i  THEN  rename_last_tac a [""] (i+1);
    22.9  
   22.10  val prems = Goal
   22.11      "[| !!x. P x 1p;  \
    23.1 --- a/src/HOL/Real/PReal.ML	Wed Aug 30 16:24:29 2000 +0200
    23.2 +++ b/src/HOL/Real/PReal.ML	Wed Aug 30 16:29:21 2000 +0200
    23.3 @@ -586,7 +586,7 @@
    23.4  Goal "ALL xa : Rep_preal(A). xa + x : Rep_preal(A) ==> \
    23.5  \            EX xb : Rep_preal(A). xb + (prat_of_pnat p)*x : Rep_preal(A)";
    23.6  by (cut_facts_tac [mem_Rep_preal_Ex] 1);
    23.7 -by (res_inst_tac [("n","p")] pnat_induct 1);
    23.8 +by (induct_thm_tac pnat_induct "p" 1);
    23.9  by (auto_tac (claset(),simpset() addsimps [pnat_one_def,
   23.10      pSuc_is_plus_one,prat_add_mult_distrib,
   23.11     prat_of_pnat_add,prat_add_assoc RS sym]));
    24.1 --- a/src/HOL/Subst/AList.ML	Wed Aug 30 16:24:29 2000 +0200
    24.2 +++ b/src/HOL/Subst/AList.ML	Wed Aug 30 16:29:21 2000 +0200
    24.3 @@ -18,5 +18,5 @@
    24.4  
    24.5  (*Perform induction on xs. *)
    24.6  fun alist_ind_tac a M = 
    24.7 -    EVERY [res_inst_tac [("l",a)] alist_induct M,
    24.8 +    EVERY [induct_thm_tac alist_induct a M,
    24.9             rename_last_tac a ["1"] (M+1)];
    25.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Aug 30 16:24:29 2000 +0200
    25.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Aug 30 16:29:21 2000 +0200
    25.3 @@ -9,6 +9,7 @@
    25.4  signature BASIC_DATATYPE_PACKAGE =
    25.5  sig
    25.6    val induct_tac : string -> int -> tactic
    25.7 +  val induct_thm_tac : thm -> string -> int -> tactic
    25.8    val case_tac : string -> int -> tactic
    25.9    val distinct_simproc : simproc
   25.10  end;
   25.11 @@ -199,6 +200,9 @@
   25.12  
   25.13  fun induct_tac s = gen_induct_tac (map (Library.single o Some) (Syntax.read_idents s), None);
   25.14  
   25.15 +fun induct_thm_tac th s =
   25.16 +  gen_induct_tac ([map Some (Syntax.read_idents s)], Some th);
   25.17 +
   25.18  end;
   25.19  
   25.20  
    26.1 --- a/src/HOL/UNITY/AllocBase.ML	Wed Aug 30 16:24:29 2000 +0200
    26.2 +++ b/src/HOL/UNITY/AllocBase.ML	Wed Aug 30 16:29:21 2000 +0200
    26.3 @@ -59,7 +59,7 @@
    26.4  
    26.5  Goal "bag_of (sublist l A) = \
    26.6  \     setsum (%i. {# l!i #}) (A Int lessThan (length l))";
    26.7 -by (res_inst_tac [("xs","l")] rev_induct 1);
    26.8 +by (rev_induct_tac "l" 1);
    26.9  by (Simp_tac 1);
   26.10  by (asm_simp_tac
   26.11      (simpset() addsimps [sublist_append, Int_insert_right, lessThan_Suc, 
    27.1 --- a/src/HOL/UNITY/GenPrefix.ML	Wed Aug 30 16:24:29 2000 +0200
    27.2 +++ b/src/HOL/UNITY/GenPrefix.ML	Wed Aug 30 16:29:21 2000 +0200
    27.3 @@ -341,7 +341,7 @@
    27.4  Addsimps [prefix_snoc];
    27.5  
    27.6  Goal "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))";
    27.7 -by (res_inst_tac [("xs","zs")] rev_induct 1);
    27.8 +by (rev_induct_tac "zs" 1);
    27.9   by (Force_tac 1);
   27.10  by (asm_full_simp_tac (simpset() delsimps [append_assoc]
   27.11                                   addsimps [append_assoc RS sym])1);
    28.1 --- a/src/HOL/While.ML	Wed Aug 30 16:24:29 2000 +0200
    28.2 +++ b/src/HOL/While.ML	Wed Aug 30 16:29:21 2000 +0200
    28.3 @@ -40,7 +40,7 @@
    28.4  \   !!s. [| P s; ~b s |] ==> Q s; \
    28.5  \   wf{(t,s). P s & b s & t = c s} |] \
    28.6  \ ==> P s --> Q(while b c s)";
    28.7 -by(res_inst_tac [("a","s")] (prem3 RS wf_induct) 1);
    28.8 +by(induct_thm_tac (prem3 RS wf_induct) "s" 1);
    28.9  by(Asm_full_simp_tac 1);
   28.10  by(Clarify_tac 1);
   28.11  by(stac while_unfold 1);
    29.1 --- a/src/HOL/ex/Factorization.ML	Wed Aug 30 16:24:29 2000 +0200
    29.2 +++ b/src/HOL/ex/Factorization.ML	Wed Aug 30 16:29:21 2000 +0200
    29.3 @@ -195,7 +195,7 @@
    29.4  qed "split_primel";
    29.5  
    29.6  Goal "1<n --> (EX l. primel l & prod l = n)"; 
    29.7 -by (res_inst_tac [("n","n")] less_induct 1);
    29.8 +by (induct_thm_tac less_induct "n" 1);
    29.9  by (rtac impI 1);
   29.10  by (case_tac "n:prime" 1);
   29.11  by (rtac exI 1);
   29.12 @@ -267,7 +267,7 @@
   29.13  
   29.14  Goal "ALL xs ys. (primel xs & primel ys & prod xs = prod ys & prod xs = n \
   29.15  \     --> xs <~~> ys)";
   29.16 -by (res_inst_tac [("n","n")] less_induct 1);
   29.17 +by (induct_thm_tac less_induct "n" 1);
   29.18  by Safe_tac;
   29.19  by (case_tac "xs" 1);
   29.20  by (force_tac (claset() addIs [primel_one_empty], simpset()) 1);
    30.1 --- a/src/HOL/ex/Fib.ML	Wed Aug 30 16:24:29 2000 +0200
    30.2 +++ b/src/HOL/ex/Fib.ML	Wed Aug 30 16:29:21 2000 +0200
    30.3 @@ -24,7 +24,7 @@
    30.4  
    30.5  (*Concrete Mathematics, page 280*)
    30.6  Goal "fib (Suc (n + k)) = fib(Suc k) * fib(Suc n) + fib k * fib n";
    30.7 -by (res_inst_tac [("x","n")] fib.induct 1);
    30.8 +by (induct_thm_tac fib.induct "n" 1);
    30.9  (*Simplify the LHS just enough to apply the induction hypotheses*)
   30.10  by (asm_full_simp_tac
   30.11      (simpset() addsimps [inst "x" "Suc(?m+?n)" fib_Suc_Suc]) 3);
   30.12 @@ -35,7 +35,7 @@
   30.13  
   30.14  
   30.15  Goal "fib (Suc n) ~= 0";
   30.16 -by (res_inst_tac [("x","n")] fib.induct 1);
   30.17 +by (induct_thm_tac fib.induct "n" 1);
   30.18  by (ALLGOALS (asm_simp_tac (simpset() addsimps [fib_Suc_Suc])));
   30.19  qed "fib_Suc_neq_0";
   30.20  
   30.21 @@ -52,7 +52,7 @@
   30.22  Goal "int (fib (Suc (Suc n)) * fib n) = \
   30.23  \     (if n mod 2 = 0 then int (fib(Suc n) * fib(Suc n)) - #1 \
   30.24  \                     else int (fib(Suc n) * fib(Suc n)) + #1)";
   30.25 -by (res_inst_tac [("x","n")] fib.induct 1);
   30.26 +by (induct_thm_tac fib.induct "n" 1);
   30.27  by (simp_tac (simpset() addsimps [fib_Suc_Suc, mod_Suc]) 2);
   30.28  by (simp_tac (simpset() addsimps [fib_Suc_Suc]) 1);
   30.29  by (asm_full_simp_tac
   30.30 @@ -65,7 +65,7 @@
   30.31  (** Towards Law 6.111 of Concrete Mathematics **)
   30.32  
   30.33  Goal "gcd(fib n, fib (Suc n)) = 1";
   30.34 -by (res_inst_tac [("x","n")] fib.induct 1);
   30.35 +by (induct_thm_tac fib.induct "n" 1);
   30.36  by (asm_simp_tac (simpset() addsimps [fib_Suc3, gcd_commute, gcd_add2]) 3);
   30.37  by (ALLGOALS (simp_tac (simpset() addsimps [fib_Suc_Suc])));
   30.38  qed "gcd_fib_Suc_eq_1"; 
   30.39 @@ -90,7 +90,7 @@
   30.40  qed "gcd_fib_diff";
   30.41  
   30.42  Goal "0<m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)";
   30.43 -by (res_inst_tac [("n","n")] less_induct 1);
   30.44 +by (induct_thm_tac less_induct "n" 1);
   30.45  by (stac mod_if 1);
   30.46  by (Asm_simp_tac 1);
   30.47  by (asm_simp_tac (simpset() addsimps [gcd_fib_diff, mod_geq, 
   30.48 @@ -99,7 +99,7 @@
   30.49  
   30.50  (*Law 6.111*)
   30.51  Goal "fib(gcd(m,n)) = gcd(fib m, fib n)";
   30.52 -by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
   30.53 +by (induct_thm_tac gcd_induct "m n" 1);
   30.54  by (Asm_simp_tac 1);
   30.55  by (asm_full_simp_tac (simpset() addsimps [gcd_non_0]) 1);
   30.56  by (asm_full_simp_tac (simpset() addsimps [gcd_commute, gcd_fib_mod]) 1);
    31.1 --- a/src/HOL/ex/Primes.ML	Wed Aug 30 16:24:29 2000 +0200
    31.2 +++ b/src/HOL/ex/Primes.ML	Wed Aug 30 16:29:21 2000 +0200
    31.3 @@ -24,7 +24,7 @@
    31.4       "[| !!m. P m 0;     \
    31.5  \        !!m n. [| 0<n;  P n (m mod n) |] ==> P m n  \
    31.6  \     |] ==> P (m::nat) (n::nat)";
    31.7 -by (res_inst_tac [("u","m"),("v","n")] gcd.induct 1);
    31.8 +by (induct_thm_tac gcd.induct "m n" 1);
    31.9  by (case_tac "n=0" 1);
   31.10  by (asm_simp_tac (simpset() addsimps prems) 1);
   31.11  by Safe_tac;
   31.12 @@ -50,7 +50,7 @@
   31.13  
   31.14  (*gcd(m,n) divides m and n.  The conjunctions don't seem provable separately*)
   31.15  Goal "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)";
   31.16 -by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
   31.17 +by (induct_thm_tac gcd_induct "m n" 1);
   31.18  by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [gcd_non_0])));
   31.19  by (blast_tac (claset() addDs [dvd_mod_imp_dvd]) 1);
   31.20  qed "gcd_dvd_both";
   31.21 @@ -62,7 +62,7 @@
   31.22  (*Maximality: for all m,n,f naturals, 
   31.23                  if f divides m and f divides n then f divides gcd(m,n)*)
   31.24  Goal "(f dvd m) --> (f dvd n) --> f dvd gcd(m,n)";
   31.25 -by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
   31.26 +by (induct_thm_tac gcd_induct "m n" 1);
   31.27  by (ALLGOALS (asm_full_simp_tac (simpset() addsimps[gcd_non_0, dvd_mod])));
   31.28  qed_spec_mp "gcd_greatest";
   31.29  
   31.30 @@ -118,7 +118,7 @@
   31.31  
   31.32  (*Davenport, page 27*)
   31.33  Goal "k * gcd(m,n) = gcd(k*m, k*n)";
   31.34 -by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
   31.35 +by (induct_thm_tac gcd_induct "m n" 1);
   31.36  by (Asm_full_simp_tac 1);
   31.37  by (case_tac "k=0" 1);
   31.38   by (Asm_full_simp_tac 1);
    32.1 --- a/src/HOL/ex/Primrec.ML	Wed Aug 30 16:24:29 2000 +0200
    32.2 +++ b/src/HOL/ex/Primrec.ML	Wed Aug 30 16:29:21 2000 +0200
    32.3 @@ -46,7 +46,7 @@
    32.4  
    32.5  (*PROPERTY A 4*)
    32.6  Goal "j < ack(i,j)";
    32.7 -by (res_inst_tac [("u","i"),("v","j")] ack.induct 1);
    32.8 +by (induct_thm_tac ack.induct "i j" 1);
    32.9  by (ALLGOALS Asm_simp_tac);
   32.10  qed "less_ack2";
   32.11  
   32.12 @@ -54,7 +54,7 @@
   32.13  
   32.14  (*PROPERTY A 5-, the single-step lemma*)
   32.15  Goal "ack(i,j) < ack(i, Suc(j))";
   32.16 -by (res_inst_tac [("u","i"),("v","j")] ack.induct 1);
   32.17 +by (induct_thm_tac ack.induct "i j" 1);
   32.18  by (ALLGOALS Asm_simp_tac);
   32.19  qed "ack_less_ack_Suc2";
   32.20  
   32.21 @@ -62,7 +62,7 @@
   32.22  
   32.23  (*PROPERTY A 5, monotonicity for < *)
   32.24  Goal "j<k --> ack(i,j) < ack(i,k)";
   32.25 -by (res_inst_tac [("u","i"),("v","k")] ack.induct 1);
   32.26 +by (induct_thm_tac ack.induct "i k" 1);
   32.27  by (ALLGOALS Asm_simp_tac);
   32.28  by (blast_tac (claset() addSEs [less_SucE] addIs [less_trans]) 1);
   32.29  qed_spec_mp "ack_less_mono2";
   32.30 @@ -115,10 +115,10 @@
   32.31  
   32.32  (*PROPERTY A 7, monotonicity for < [not clear why ack_1 is now needed first!]*)
   32.33  Goal "ack(i,k) < ack(Suc(i+i'),k)";
   32.34 -by (res_inst_tac [("u","i"),("v","k")] ack.induct 1);
   32.35 +by (induct_thm_tac ack.induct "i k" 1);
   32.36  by (ALLGOALS Asm_full_simp_tac);
   32.37  by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 2);
   32.38 -by (res_inst_tac [("u","i'"),("v","n")] ack.induct 1);
   32.39 +by (induct_thm_tac ack.induct "i' n" 1);
   32.40  by (ALLGOALS Asm_simp_tac);
   32.41  by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 1);
   32.42  by (blast_tac (claset() addIs [Suc_leI RS le_less_trans, ack_less_mono2]) 1);
    33.1 --- a/src/HOL/ex/Puzzle.ML	Wed Aug 30 16:24:29 2000 +0200
    33.2 +++ b/src/HOL/ex/Puzzle.ML	Wed Aug 30 16:29:21 2000 +0200
    33.3 @@ -11,7 +11,7 @@
    33.4  AddSIs [Puzzle.f_ax];
    33.5  
    33.6  Goal "! n. k=f(n) --> n <= f(n)";
    33.7 -by (res_inst_tac [("n","k")] less_induct 1);
    33.8 +by (induct_thm_tac less_induct "k" 1);
    33.9  by (rtac allI 1);
   33.10  by (rename_tac "i" 1);
   33.11  by (case_tac "i" 1);
    34.1 --- a/src/HOL/ex/Qsort.ML	Wed Aug 30 16:24:29 2000 +0200
    34.2 +++ b/src/HOL/ex/Qsort.ML	Wed Aug 30 16:29:21 2000 +0200
    34.3 @@ -9,7 +9,7 @@
    34.4  (*** Version one: higher-order ***)
    34.5  
    34.6  Goal "multiset (qsort(le,xs)) x = multiset xs x";
    34.7 -by (res_inst_tac [("v","xs"),("u","le")] qsort.induct 1);
    34.8 +by (induct_thm_tac qsort.induct "le xs" 1);
    34.9  by Auto_tac;
   34.10  qed "qsort_permutes";
   34.11  Addsimps [qsort_permutes];
   34.12 @@ -21,7 +21,7 @@
   34.13  Addsimps [set_qsort];
   34.14  
   34.15  Goal "total(le) --> transf(le) --> sorted le (qsort(le,xs))";
   34.16 -by (res_inst_tac [("v","xs"),("u","le")] qsort.induct 1);
   34.17 +by (induct_thm_tac qsort.induct "le xs" 1);
   34.18  by (ALLGOALS Asm_simp_tac);
   34.19  by (rewrite_goals_tac [Sorting.total_def, Sorting.transf_def]);
   34.20  by (Blast_tac 1);
    35.1 --- a/src/HOL/ex/Recdefs.ML	Wed Aug 30 16:24:29 2000 +0200
    35.2 +++ b/src/HOL/ex/Recdefs.ML	Wed Aug 30 16:29:21 2000 +0200
    35.3 @@ -12,12 +12,12 @@
    35.4  Addsimps g.simps;
    35.5  
    35.6  Goal "g x < Suc x";
    35.7 -by (res_inst_tac [("x","x")] g.induct 1);
    35.8 +by (induct_thm_tac g.induct "x" 1);
    35.9  by Auto_tac;
   35.10  qed "g_terminates";
   35.11  
   35.12  Goal "g x = 0";
   35.13 -by (res_inst_tac [("x","x")] g.induct 1);
   35.14 +by (induct_thm_tac g.induct "x" 1);
   35.15  by (ALLGOALS (asm_simp_tac (simpset() addsimps [g_terminates])));
   35.16  qed "g_zero";
   35.17