# HG changeset patch
# User nipkow
# Date 967645761 -7200
# Node ID 043098ba5098c4b7a2fa12799b919ca44f5a873b
# Parent  64b803edef396c5897eb080549cb76330f1e2eca
introduced induct_thm_tac

diff -r 64b803edef39 -r 043098ba5098 src/HOL/IMP/Transition.ML
--- a/src/HOL/IMP/Transition.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/IMP/Transition.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -93,7 +93,7 @@
 (* WHILE, induction on the length of the computation *)
 by (eres_inst_tac [("P","?X -n-> ?Y")] rev_mp 1);
 by (res_inst_tac [("x","s")] spec 1);
-by (res_inst_tac [("n","n")] less_induct 1);
+by (induct_thm_tac less_induct "n" 1);
 by (strip_tac 1);
 by (etac rel_pow_E2 1);
  by (Asm_full_simp_tac 1);
@@ -214,7 +214,7 @@
 qed_spec_mp "comp_decomp_lemma";
 
 Goal "!c s t. (c,s) -n-> (SKIP,t) --> <c,s> -c-> t";
-by (res_inst_tac [("n","n")] less_induct 1);
+by (induct_thm_tac less_induct "n" 1);
 by (Clarify_tac 1);
 by (etac rel_pow_E2 1);
  by (asm_full_simp_tac (simpset() addsimps evalc.intrs) 1);
diff -r 64b803edef39 -r 043098ba5098 src/HOL/Induct/LList.ML
--- a/src/HOL/Induct/LList.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Induct/LList.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -128,7 +128,7 @@
 qed "LListD_unfold";
 
 Goal "!M N. (M,N) : LListD(diag A) --> ntrunc k M = ntrunc k N";
-by (res_inst_tac [("n", "k")] less_induct 1);
+by (induct_thm_tac less_induct "k" 1);
 by (safe_tac (claset() delrules [equalityI]));
 by (etac LListD.elim 1);
 by (safe_tac (claset() delrules [equalityI]));
@@ -287,7 +287,7 @@
 by (rtac (ntrunc_equality RS ext) 1);
 by (rename_tac "x k" 1);
 by (res_inst_tac [("x", "x")] spec 1);
-by (res_inst_tac [("n", "k")] less_induct 1);
+by (induct_thm_tac less_induct "k" 1);
 by (rename_tac "n" 1);
 by (rtac allI 1);
 by (rename_tac "y" 1);
diff -r 64b803edef39 -r 043098ba5098 src/HOL/Induct/Multiset.ML
--- a/src/HOL/Induct/Multiset.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Induct/Multiset.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -457,7 +457,7 @@
 by (Clarify_tac 1);
 by (rotate_tac ~1 1);
 by (etac rev_mp 1);
-by (res_inst_tac [("M","K")] multiset_induct 1);
+by (induct_thm_tac multiset_induct "K" 1);
  by (Asm_simp_tac 1);
 by (simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
 by (Blast_tac 1);
@@ -476,7 +476,7 @@
 qed "lemma3";
 
 Goalw [W_def] "wf(r) ==> M : W";
-by (res_inst_tac [("M","M")] multiset_induct 1);
+by (induct_thm_tac multiset_induct "M" 1);
  by (rtac accI 1);
  by (Asm_full_simp_tac 1);
 by (blast_tac (claset() addDs [export lemma3]) 1);
diff -r 64b803edef39 -r 043098ba5098 src/HOL/Induct/Perm.ML
--- a/src/HOL/Induct/Perm.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Induct/Perm.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -145,7 +145,7 @@
 AddIffs [cons_perm_eq];
 
 Goal "ALL xs ys. zs@xs <~~> zs@ys --> xs <~~> ys";
-by (res_inst_tac [("xs","zs")] rev_induct 1);
+by (rev_induct_tac "zs" 1);
 by (ALLGOALS Full_simp_tac);
 by (Blast_tac 1);
 qed_spec_mp "append_perm_imp_perm";
diff -r 64b803edef39 -r 043098ba5098 src/HOL/Induct/SList.ML
--- a/src/HOL/Induct/SList.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Induct/SList.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -52,7 +52,7 @@
 
 (*Perform induction on xs. *)
 fun list_ind_tac a M = 
-    EVERY [res_inst_tac [("l",a)] list_induct2 M,
+    EVERY [induct_thm_tac list_induct2 a M,
            rename_last_tac a ["1"] (M+1)];
 
 (*** Isomorphisms ***)
diff -r 64b803edef39 -r 043098ba5098 src/HOL/Integ/IntDiv.ML
--- a/src/HOL/Integ/IntDiv.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Integ/IntDiv.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -113,7 +113,7 @@
 
 (*Correctness of posDivAlg: it computes quotients correctly*)
 Goal "#0 <= a --> #0 < b --> quorem ((a, b), posDivAlg (a, b))";
-by (res_inst_tac [("u", "a"), ("v", "b")] posDivAlg_induct 1);
+by (induct_thm_tac posDivAlg_induct "a b" 1);
 by Auto_tac;
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def])));
 (*base case: a<b*)
@@ -152,7 +152,7 @@
 (*Correctness of negDivAlg: it computes quotients correctly
   It doesn't work if a=0 because the 0/b=0 rather than -1*)
 Goal "a < #0 --> #0 < b --> quorem ((a, b), negDivAlg (a, b))";
-by (res_inst_tac [("u", "a"), ("v", "b")] negDivAlg_induct 1);
+by (induct_thm_tac negDivAlg_induct "a b" 1);
 by Auto_tac;
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def])));
 (*base case: 0<=a+b*)
diff -r 64b803edef39 -r 043098ba5098 src/HOL/Integ/int_arith2.ML
--- a/src/HOL/Integ/int_arith2.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Integ/int_arith2.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -88,7 +88,7 @@
 
 (*Analogous to zadd_int, but more easily provable using the arithmetic in Bin*)
 Goal "n<=m --> int m - int n = int (m-n)";
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (induct_thm_tac diff_induct "m n" 1);
 by Auto_tac;
 qed_spec_mp "zdiff_int";
 
diff -r 64b803edef39 -r 043098ba5098 src/HOL/Lambda/ListApplication.ML
--- a/src/HOL/Lambda/ListApplication.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Lambda/ListApplication.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -97,7 +97,7 @@
 "[| !!n ts. !t : set ts. P t ==> P((Var n)$$ts); \
 \   !!u ts. [| P u; !t : set ts. P t |] ==> P((Abs u)$$ts) \
 \|] ==> !t. size t = n --> P t";
-by (res_inst_tac [("n","n")] less_induct 1);
+by (induct_thm_tac less_induct "n" 1);
 by (rtac allI 1);
 by (cut_inst_tac [("t","t")] ex_head_tail 1);
 by (Clarify_tac 1);
diff -r 64b803edef39 -r 043098ba5098 src/HOL/Lambda/ListBeta.ML
--- a/src/HOL/Lambda/ListBeta.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Lambda/ListBeta.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -66,7 +66,7 @@
 AddSEs [apps_betasE];
 
 Goal "r -> s ==> r$$ss -> s$$ss";
-by (res_inst_tac [("xs","ss")] rev_induct 1);
+by (rev_induct_tac "ss" 1);
 by (Auto_tac);
 qed "apps_preserves_beta";
 Addsimps [apps_preserves_beta];
@@ -79,7 +79,7 @@
 Addsimps [apps_preserves_beta2];
 
 Goal "!ss. rs => ss --> r$$rs -> r$$ss";
-by (res_inst_tac [("xs","rs")] rev_induct 1);
+by (rev_induct_tac "rs" 1);
  by (Asm_full_simp_tac 1);
 by (Asm_full_simp_tac 1);
 by (Clarify_tac 1);
diff -r 64b803edef39 -r 043098ba5098 src/HOL/Lambda/ParRed.ML
--- a/src/HOL/Lambda/ParRed.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Lambda/ParRed.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -83,7 +83,7 @@
 (*** cd ***)
 
 Goal "!t. s => t --> t => cd s";
-by (res_inst_tac[("x","s")] cd.induct 1);
+by (induct_thm_tac cd.induct "s" 1);
 by (Auto_tac);
 by (fast_tac (claset() addSIs [par_beta_subst]) 1);
 qed_spec_mp "par_beta_cd";
diff -r 64b803edef39 -r 043098ba5098 src/HOL/Lex/MaxChop.ML
--- a/src/HOL/Lex/MaxChop.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Lex/MaxChop.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -33,7 +33,7 @@
 
 Goal "is_maxsplitter P splitf ==> \
 \ !yss zs. chop splitf xs = (yss,zs) --> xs = concat yss @ zs";
-by (res_inst_tac [("xs","xs")] length_induct 1);
+by (induct_thm_tac length_induct "xs" 1);
 by (asm_simp_tac (simpset() delsplits [split_if]
                            addsimps [chop_rule,is_maxsplitter_reducing]) 1);
 by (asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
@@ -42,7 +42,7 @@
 
 Goal "is_maxsplitter P splitf ==> \
 \ !yss zs. chop splitf xs = (yss,zs) --> (!ys : set yss. ys ~= [])";
-by (res_inst_tac [("xs","xs")] length_induct 1);
+by (induct_thm_tac length_induct "xs" 1);
 by (asm_simp_tac (simpset() addsimps [chop_rule,is_maxsplitter_reducing]) 1);
 by (asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
                                  addsplits [split_split]) 1);
diff -r 64b803edef39 -r 043098ba5098 src/HOL/Lex/Prefix.ML
--- a/src/HOL/Lex/Prefix.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Lex/Prefix.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -81,7 +81,7 @@
 qed "prefix_Cons";
 
 Goal "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))";
-by (res_inst_tac [("xs","zs")] rev_induct 1);
+by (rev_induct_tac "zs" 1);
  by (Force_tac 1);
 by (asm_full_simp_tac (simpset() delsimps [append_assoc]
                                  addsimps [append_assoc RS sym])1);
diff -r 64b803edef39 -r 043098ba5098 src/HOL/Lex/RegExp2NAe.ML
--- a/src/HOL/Lex/RegExp2NAe.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Lex/RegExp2NAe.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -500,7 +500,7 @@
 \ (? us v. w = concat us @ v & \
 \             (!u:set us. accepts A u) & \
 \             (? r. (start A,r) : steps A v & rr = True#r))";
-by (res_inst_tac [("xs","w")] rev_induct 1);
+by (rev_induct_tac "w" 1);
  by (Asm_full_simp_tac 1);
  by (Clarify_tac 1);
  by (res_inst_tac [("x","[]")] exI 1);
diff -r 64b803edef39 -r 043098ba5098 src/HOL/List.ML
--- a/src/HOL/List.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/List.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -414,10 +414,10 @@
 by (eresolve_tac prems 1);
 qed "rev_induct";
 
-fun rev_induct_tac xs = res_inst_tac [("xs",xs)] rev_induct;
+val rev_induct_tac = induct_thm_tac rev_induct;
 
 Goal  "(xs = [] --> P) -->  (!ys y. xs = ys@[y] --> P) --> P";
-by (res_inst_tac [("xs","xs")] rev_induct 1);
+by (rev_induct_tac "xs" 1);
 by Auto_tac;
 bind_thm ("rev_exhaust",
   impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp)))));
@@ -752,7 +752,7 @@
 Addsimps [butlast_snoc];
 
 Goal "length(butlast xs) = length xs - 1";
-by (res_inst_tac [("xs","xs")] rev_induct 1);
+by (rev_induct_tac "xs" 1);
 by Auto_tac;
 qed "length_butlast";
 Addsimps [length_butlast];
@@ -1217,7 +1217,7 @@
 qed "map_Suc_upt";
 
 Goal "ALL i. i < n-m --> (map f [m..n(]) ! i = f(m+i)";
-by (res_inst_tac [("m","n"),("n","m")] diff_induct 1);
+by (induct_thm_tac diff_induct "n m" 1);
 by (stac (map_Suc_upt RS sym) 3);
 by (auto_tac (claset(), simpset() addsimps [less_diff_conv, nth_upt]));
 qed_spec_mp "nth_map_upt";
@@ -1453,14 +1453,14 @@
 
 Goal "map fst [p:zip xs [i..i + length xs(] . snd p : A] =     \
 \     map fst [p:zip xs [0..length xs(] . snd p + i : A]";
-by (res_inst_tac [("xs","xs")] rev_induct 1);
+by (rev_induct_tac "xs" 1);
  by (asm_simp_tac (simpset() addsimps [add_commute]) 2);
 by (Simp_tac 1);
 qed "sublist_shift_lemma";
 
 Goalw [sublist_def]
      "sublist (l@l') A = sublist l A @ sublist l' {j. j + length l : A}";
-by (res_inst_tac [("xs","l'")] rev_induct 1);
+by (rev_induct_tac "l'" 1);
 by (Simp_tac 1);
 by (asm_simp_tac (simpset() addsimps [inst "i" "0" upt_add_eq_append, 
 	                              zip_append, sublist_shift_lemma]) 1);
@@ -1470,7 +1470,7 @@
 Addsimps [sublist_empty, sublist_nil];
 
 Goal "sublist (x#l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}";
-by (res_inst_tac [("xs","l")] rev_induct 1);
+by (rev_induct_tac "l" 1);
  by (asm_simp_tac (simpset() delsimps [append_Cons]
 	 		     addsimps [append_Cons RS sym, sublist_append]) 2);
 by (simp_tac (simpset() addsimps [sublist_def]) 1);
@@ -1482,7 +1482,7 @@
 Addsimps [sublist_singleton];
 
 Goal "sublist l {..n(} = take n l";
-by (res_inst_tac [("xs","l")] rev_induct 1);
+by (rev_induct_tac "l" 1);
  by (asm_simp_tac (simpset() addsplits [nat_diff_split]
                              addsimps [sublist_append]) 2);
 by (Simp_tac 1);
diff -r 64b803edef39 -r 043098ba5098 src/HOL/MiniML/MiniML.ML
--- a/src/HOL/MiniML/MiniML.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/MiniML/MiniML.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -114,7 +114,7 @@
 qed "free_tv_alpha";
 
 Goal "!!(k::nat). n <= n + k";
-by (res_inst_tac [("n","k")] nat_induct 1);
+by (induct_thm_tac nat_induct "k" 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
 val aux_plus = result();
diff -r 64b803edef39 -r 043098ba5098 src/HOL/MiniML/Type.ML
--- a/src/HOL/MiniML/Type.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/MiniML/Type.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -150,7 +150,7 @@
 by (induct_tac "A" 1);
 by (Asm_full_simp_tac 1);
 by (rtac allI 1);
-by (res_inst_tac [("n","n")] nat_induct 1);
+by (induct_thm_tac nat_induct "n" 1);
 by (Asm_full_simp_tac 1);
 by (Asm_full_simp_tac 1);
 qed_spec_mp "free_tv_nth_A_impl_free_tv_A";
@@ -161,7 +161,7 @@
 by (induct_tac "A" 1);
 by (Asm_full_simp_tac 1);
 by (rtac allI 1);
-by (res_inst_tac [("n","nat")] nat_induct 1);
+by (induct_thm_tac nat_induct "nat" 1);
 by (strip_tac 1);
 by (Asm_full_simp_tac 1);
 by (Simp_tac 1);
@@ -505,7 +505,7 @@
 by (induct_tac "A" 1);
 by (Asm_full_simp_tac 1);
 by (rtac allI 1);
-by (res_inst_tac [("n","nat")] nat_induct 1);
+by (induct_thm_tac nat_induct "nat" 1);
 by (strip_tac 1);
 by (Asm_full_simp_tac 1);
 by (Simp_tac 1);
@@ -718,7 +718,7 @@
 by (Asm_full_simp_tac 1);
 by (rtac allI 1);
 by (rename_tac "n1" 1);
-by (res_inst_tac[("n","n1")] nat_induct 1);
+by (induct_thm_tac nat_induct "n1" 1);
 by (Asm_full_simp_tac 1);
 by (Asm_full_simp_tac 1);
 qed_spec_mp "nth_subst";
diff -r 64b803edef39 -r 043098ba5098 src/HOL/NumberTheory/EulerFermat.ML
--- a/src/HOL/NumberTheory/EulerFermat.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/NumberTheory/EulerFermat.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -30,7 +30,7 @@
 qed "BnorRset_induct";
 
 Goal "b:BnorRset(a,m) --> b<=a";
-by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
+by (induct_thm_tac BnorRset_induct "a m" 1);
 by (stac BnorRset_eq 2);
 by (rewtac Let_def);
 by Auto_tac;
@@ -43,14 +43,14 @@
 qed "Bnor_mem_zle_swap";
 
 Goal "b:BnorRset(a,m) --> #0<b";
-by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
+by (induct_thm_tac BnorRset_induct "a m" 1);
 by (stac BnorRset_eq 2);
 by (rewtac Let_def);
 by Auto_tac;
 qed_spec_mp "Bnor_mem_zg"; 
 
 Goal "zgcd(b,m) = #1 --> #0<b --> b<=a --> b:BnorRset(a,m)";
-by (res_inst_tac [("u","a"),("v","m")] BnorRset.induct 1);
+by (induct_thm_tac BnorRset.induct "a m" 1);
 by Auto_tac;
 by (case_tac "a=b" 1);
 by (asm_full_simp_tac (simpset() addsimps [zle_neq_implies_zless]) 2);
@@ -61,7 +61,7 @@
 qed_spec_mp "Bnor_mem_if";
 
 Goal "a<m --> BnorRset (a,m) : RsetR m";
-by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
+by (induct_thm_tac BnorRset_induct "a m" 1);
 by (Simp_tac 1);
 by (stac BnorRset_eq 1);
 by (rewtac Let_def);
@@ -77,7 +77,7 @@
 qed_spec_mp "Bnor_in_RsetR";
 
 Goal "finite (BnorRset (a,m))";
-by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
+by (induct_thm_tac BnorRset_induct "a m" 1);
 by (stac BnorRset_eq 2);
 by (rewtac Let_def);
 by Auto_tac;
@@ -210,7 +210,7 @@
 
 Goal "x~=#0 ==> a<m --> setprod ((%a. a*x) `` BnorRset(a,m)) = \
 \     setprod (BnorRset(a,m)) * x^card(BnorRset(a,m))";
-by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
+by (induct_thm_tac BnorRset_induct "a m" 1);
 by (stac BnorRset_eq 2);
 by (rewtac Let_def);
 by Auto_tac;
@@ -235,7 +235,7 @@
 
 Goalw [norRRset_def,phi_def]
       "#0<m --> a<m --> zgcd (setprod (BnorRset (a,m)),m) = #1";
-by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
+by (induct_thm_tac BnorRset_induct "a m" 1);
 by (stac BnorRset_eq 2);
 by (rewtac Let_def);
 by Auto_tac;
@@ -270,7 +270,7 @@
 Goalw [zprime_def] 
       "p:zprime ==> a<p --> (ALL b. #0<b & b<=a --> zgcd(b,p) = #1) \
 \      --> card (BnorRset(a, p)) = nat a";
-by (res_inst_tac [("u","a"),("v","p")] BnorRset.induct 1);
+by (induct_thm_tac BnorRset.induct "a p" 1);
 by (stac BnorRset_eq 1);
 by (rewtac Let_def);
 by Auto_tac;
diff -r 64b803edef39 -r 043098ba5098 src/HOL/NumberTheory/IntFact.ML
--- a/src/HOL/NumberTheory/IntFact.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/NumberTheory/IntFact.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -42,13 +42,13 @@
 qed "d22set_induct";
 
 Goal "b:(d22set a) --> #1<b";
-by (res_inst_tac [("u","a")] d22set_induct 1);
+by (induct_thm_tac d22set_induct "a" 1);
 by (stac d22set_eq 2);
 by Auto_tac;
 qed_spec_mp "d22set_g_1";
 
 Goal "b:(d22set a) --> b<=a";
-by (res_inst_tac [("u","a")] d22set_induct 1);
+by (induct_thm_tac d22set_induct "a" 1);
 by (stac d22set_eq 2);
 by Auto_tac;
 qed_spec_mp "d22set_le";
@@ -60,13 +60,13 @@
 qed "d22set_le_swap";
 
 Goal "#1<b --> b<=a --> b:(d22set a)";
-by (res_inst_tac [("x","a")] d22set.induct 1);
+by (induct_thm_tac d22set.induct "a" 1);
 by Auto_tac;
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [d22set_eq])));
 qed_spec_mp "d22set_mem";
 
 Goal "finite (d22set a)";
-by (res_inst_tac [("u","a")] d22set_induct 1);
+by (induct_thm_tac d22set_induct "a" 1);
 by (stac d22set_eq 2);
 by Auto_tac;
 qed "d22set_fin";
@@ -75,7 +75,7 @@
 Delsimps zfact.simps; 
 
 Goal "setprod(d22set a) = zfact a";
-by (res_inst_tac [("x","a")] d22set.induct 1);
+by (induct_thm_tac d22set.induct "a" 1);
 by Safe_tac;
 by (asm_full_simp_tac (simpset() addsimps [d22set_eq,zfact_eq]) 1);
 by (stac d22set_eq 1);
diff -r 64b803edef39 -r 043098ba5098 src/HOL/NumberTheory/IntPrimes.ML
--- a/src/HOL/NumberTheory/IntPrimes.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -181,7 +181,7 @@
 Addsimps [zgcd_0_1_iff];
 
 Goal "#0<=(n::int) --> (zgcd(m,n) dvd m) & (zgcd(m,n) dvd n)";
-by (res_inst_tac [("u","m"),("v","n")] zgcd.induct 1);
+by (induct_thm_tac zgcd.induct "m n" 1);
 by (case_tac "n=#0" 1);
 by (auto_tac (claset() addDs [zdvd_zmod_imp_zdvd],
               simpset() addsimps [zle_neq_implies_zless,neq_commute,
@@ -198,14 +198,14 @@
 val lemma_false = result();
 
 Goal "#0<=(n::int) --> (f dvd m) --> (f dvd n) --> f dvd zgcd(m,n)";
-by (res_inst_tac [("u","m"),("v","n")] zgcd.induct 1);
+by (induct_thm_tac zgcd.induct "m n" 1);
 by (case_tac "n=#0" 1);
 by (auto_tac (claset() addDs [lemma_false] addIs [pos_mod_sign,zdvd_zmod],
         simpset() addsimps [zgcd_non_0,neq_commute,zle_neq_implies_zless]));
 qed_spec_mp "zgcd_greatest";
 
 Goal "#0 < (n::int) --> #0 < zgcd (m, n)";
-by (res_inst_tac [("u","m"),("v","n")] zgcd.induct 1);
+by (induct_thm_tac zgcd.induct "m n" 1);
 by (auto_tac (claset(), simpset() addsimps zgcd.simps));
 qed_spec_mp "zgcd_zless";
 
@@ -269,7 +269,7 @@
 qed "zgcd_assoc";
 
 Goal "#0<=(n::int) --> #0<=k --> k * zgcd(m,n) = zgcd(k*m, k*n)";
-by (res_inst_tac [("u","m"),("v","n")] zgcd.induct 1);
+by (induct_thm_tac zgcd.induct "m n" 1);
 by (case_tac "n=#0" 1);
 by (auto_tac (claset() addDs [lemma_false],
               simpset() addsimps [zle_neq_implies_zless,pos_mod_sign,
diff -r 64b803edef39 -r 043098ba5098 src/HOL/NumberTheory/WilsonRuss.ML
--- a/src/HOL/NumberTheory/WilsonRuss.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/NumberTheory/WilsonRuss.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -175,7 +175,7 @@
 qed "wset_subset";
 
 Goal "p:zprime --> a<p-#1 --> b:(wset(a,p)) --> #1<b";
-by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
+by (induct_thm_tac wset_induct "a p" 1);
 by Auto_tac;
 by (case_tac "b=a" 1);
 by (case_tac "b=inv p a" 2);
@@ -187,7 +187,7 @@
 qed_spec_mp "wset_g_1";
 
 Goal "p:zprime --> a<p-#1 --> b:(wset(a,p)) --> b<p-#1";
-by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
+by (induct_thm_tac wset_induct "a p" 1);
 by Auto_tac;
 by (case_tac "b=a" 1);
 by (case_tac "b=inv p a" 2);
@@ -199,7 +199,7 @@
 qed_spec_mp "wset_less";
 
 Goal "p:zprime --> a<p-#1 --> #1<b --> b<=a --> b:(wset(a,p))"; 
-by (res_inst_tac [("u","a"),("v","p")] wset.induct 1);
+by (induct_thm_tac wset.induct "a p" 1);
 by Auto_tac;
 by (subgoal_tac "b=a" 1);
 by (rtac zle_anti_sym 2);
@@ -210,7 +210,7 @@
 
 Goal "p:zprime --> #5<=p --> a<p-#1 --> b:(wset (a,p)) \
 \     --> (inv p b):(wset (a,p))";
-by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
+by (induct_thm_tac wset_induct "a p" 1);
 by Auto_tac;
 by (case_tac "b=a" 1);
 by (stac wset_eq 1);
@@ -234,14 +234,14 @@
 qed "wset_inv_mem_mem";
 
 Goal "finite (wset (a,p))";
-by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
+by (induct_thm_tac wset_induct "a p" 1);
 by (stac wset_eq 2);
 by (rewtac Let_def);
 by Auto_tac;
 qed "wset_fin";
 
 Goal "p:zprime --> #5<=p --> a<p-#1 --> [setprod (wset (a,p)) = #1](mod p)";
-by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
+by (induct_thm_tac wset_induct "a p" 1);
 by (stac wset_eq 2);
 by (rewtac Let_def);
 by Auto_tac;
diff -r 64b803edef39 -r 043098ba5098 src/HOL/Real/Hyperreal/Zorn.ML
--- a/src/HOL/Real/Hyperreal/Zorn.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Real/Hyperreal/Zorn.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -53,7 +53,7 @@
 
 (*Perform induction on n, then prove the major premise using prems. *)
 fun TFin_ind_tac a prems i = 
-    EVERY [res_inst_tac [("n",a)] TFin_induct i,
+    EVERY [induct_thm_tac TFin_induct a i,
            rename_last_tac a ["1"] (i+1),
            rename_last_tac a ["2"] (i+2),
            ares_tac prems i];
diff -r 64b803edef39 -r 043098ba5098 src/HOL/Real/PNat.ML
--- a/src/HOL/Real/PNat.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Real/PNat.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -48,7 +48,7 @@
 
 (*Perform induction on n. *)
 fun pnat_ind_tac a i = 
-  res_inst_tac [("n",a)] pnat_induct i  THEN  rename_last_tac a [""] (i+1);
+  induct_thm_tac pnat_induct a i  THEN  rename_last_tac a [""] (i+1);
 
 val prems = Goal
     "[| !!x. P x 1p;  \
diff -r 64b803edef39 -r 043098ba5098 src/HOL/Real/PReal.ML
--- a/src/HOL/Real/PReal.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Real/PReal.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -586,7 +586,7 @@
 Goal "ALL xa : Rep_preal(A). xa + x : Rep_preal(A) ==> \
 \            EX xb : Rep_preal(A). xb + (prat_of_pnat p)*x : Rep_preal(A)";
 by (cut_facts_tac [mem_Rep_preal_Ex] 1);
-by (res_inst_tac [("n","p")] pnat_induct 1);
+by (induct_thm_tac pnat_induct "p" 1);
 by (auto_tac (claset(),simpset() addsimps [pnat_one_def,
     pSuc_is_plus_one,prat_add_mult_distrib,
    prat_of_pnat_add,prat_add_assoc RS sym]));
diff -r 64b803edef39 -r 043098ba5098 src/HOL/Subst/AList.ML
--- a/src/HOL/Subst/AList.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Subst/AList.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -18,5 +18,5 @@
 
 (*Perform induction on xs. *)
 fun alist_ind_tac a M = 
-    EVERY [res_inst_tac [("l",a)] alist_induct M,
+    EVERY [induct_thm_tac alist_induct a M,
            rename_last_tac a ["1"] (M+1)];
diff -r 64b803edef39 -r 043098ba5098 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -9,6 +9,7 @@
 signature BASIC_DATATYPE_PACKAGE =
 sig
   val induct_tac : string -> int -> tactic
+  val induct_thm_tac : thm -> string -> int -> tactic
   val case_tac : string -> int -> tactic
   val distinct_simproc : simproc
 end;
@@ -199,6 +200,9 @@
 
 fun induct_tac s = gen_induct_tac (map (Library.single o Some) (Syntax.read_idents s), None);
 
+fun induct_thm_tac th s =
+  gen_induct_tac ([map Some (Syntax.read_idents s)], Some th);
+
 end;
 
 
diff -r 64b803edef39 -r 043098ba5098 src/HOL/UNITY/AllocBase.ML
--- a/src/HOL/UNITY/AllocBase.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/UNITY/AllocBase.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -59,7 +59,7 @@
 
 Goal "bag_of (sublist l A) = \
 \     setsum (%i. {# l!i #}) (A Int lessThan (length l))";
-by (res_inst_tac [("xs","l")] rev_induct 1);
+by (rev_induct_tac "l" 1);
 by (Simp_tac 1);
 by (asm_simp_tac
     (simpset() addsimps [sublist_append, Int_insert_right, lessThan_Suc, 
diff -r 64b803edef39 -r 043098ba5098 src/HOL/UNITY/GenPrefix.ML
--- a/src/HOL/UNITY/GenPrefix.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/UNITY/GenPrefix.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -341,7 +341,7 @@
 Addsimps [prefix_snoc];
 
 Goal "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))";
-by (res_inst_tac [("xs","zs")] rev_induct 1);
+by (rev_induct_tac "zs" 1);
  by (Force_tac 1);
 by (asm_full_simp_tac (simpset() delsimps [append_assoc]
                                  addsimps [append_assoc RS sym])1);
diff -r 64b803edef39 -r 043098ba5098 src/HOL/While.ML
--- a/src/HOL/While.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/While.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -40,7 +40,7 @@
 \   !!s. [| P s; ~b s |] ==> Q s; \
 \   wf{(t,s). P s & b s & t = c s} |] \
 \ ==> P s --> Q(while b c s)";
-by(res_inst_tac [("a","s")] (prem3 RS wf_induct) 1);
+by(induct_thm_tac (prem3 RS wf_induct) "s" 1);
 by(Asm_full_simp_tac 1);
 by(Clarify_tac 1);
 by(stac while_unfold 1);
diff -r 64b803edef39 -r 043098ba5098 src/HOL/ex/Factorization.ML
--- a/src/HOL/ex/Factorization.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/ex/Factorization.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -195,7 +195,7 @@
 qed "split_primel";
 
 Goal "1<n --> (EX l. primel l & prod l = n)"; 
-by (res_inst_tac [("n","n")] less_induct 1);
+by (induct_thm_tac less_induct "n" 1);
 by (rtac impI 1);
 by (case_tac "n:prime" 1);
 by (rtac exI 1);
@@ -267,7 +267,7 @@
 
 Goal "ALL xs ys. (primel xs & primel ys & prod xs = prod ys & prod xs = n \
 \     --> xs <~~> ys)";
-by (res_inst_tac [("n","n")] less_induct 1);
+by (induct_thm_tac less_induct "n" 1);
 by Safe_tac;
 by (case_tac "xs" 1);
 by (force_tac (claset() addIs [primel_one_empty], simpset()) 1);
diff -r 64b803edef39 -r 043098ba5098 src/HOL/ex/Fib.ML
--- a/src/HOL/ex/Fib.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/ex/Fib.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -24,7 +24,7 @@
 
 (*Concrete Mathematics, page 280*)
 Goal "fib (Suc (n + k)) = fib(Suc k) * fib(Suc n) + fib k * fib n";
-by (res_inst_tac [("x","n")] fib.induct 1);
+by (induct_thm_tac fib.induct "n" 1);
 (*Simplify the LHS just enough to apply the induction hypotheses*)
 by (asm_full_simp_tac
     (simpset() addsimps [inst "x" "Suc(?m+?n)" fib_Suc_Suc]) 3);
@@ -35,7 +35,7 @@
 
 
 Goal "fib (Suc n) ~= 0";
-by (res_inst_tac [("x","n")] fib.induct 1);
+by (induct_thm_tac fib.induct "n" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [fib_Suc_Suc])));
 qed "fib_Suc_neq_0";
 
@@ -52,7 +52,7 @@
 Goal "int (fib (Suc (Suc n)) * fib n) = \
 \     (if n mod 2 = 0 then int (fib(Suc n) * fib(Suc n)) - #1 \
 \                     else int (fib(Suc n) * fib(Suc n)) + #1)";
-by (res_inst_tac [("x","n")] fib.induct 1);
+by (induct_thm_tac fib.induct "n" 1);
 by (simp_tac (simpset() addsimps [fib_Suc_Suc, mod_Suc]) 2);
 by (simp_tac (simpset() addsimps [fib_Suc_Suc]) 1);
 by (asm_full_simp_tac
@@ -65,7 +65,7 @@
 (** Towards Law 6.111 of Concrete Mathematics **)
 
 Goal "gcd(fib n, fib (Suc n)) = 1";
-by (res_inst_tac [("x","n")] fib.induct 1);
+by (induct_thm_tac fib.induct "n" 1);
 by (asm_simp_tac (simpset() addsimps [fib_Suc3, gcd_commute, gcd_add2]) 3);
 by (ALLGOALS (simp_tac (simpset() addsimps [fib_Suc_Suc])));
 qed "gcd_fib_Suc_eq_1"; 
@@ -90,7 +90,7 @@
 qed "gcd_fib_diff";
 
 Goal "0<m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)";
-by (res_inst_tac [("n","n")] less_induct 1);
+by (induct_thm_tac less_induct "n" 1);
 by (stac mod_if 1);
 by (Asm_simp_tac 1);
 by (asm_simp_tac (simpset() addsimps [gcd_fib_diff, mod_geq, 
@@ -99,7 +99,7 @@
 
 (*Law 6.111*)
 Goal "fib(gcd(m,n)) = gcd(fib m, fib n)";
-by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
+by (induct_thm_tac gcd_induct "m n" 1);
 by (Asm_simp_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [gcd_non_0]) 1);
 by (asm_full_simp_tac (simpset() addsimps [gcd_commute, gcd_fib_mod]) 1);
diff -r 64b803edef39 -r 043098ba5098 src/HOL/ex/Primes.ML
--- a/src/HOL/ex/Primes.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/ex/Primes.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -24,7 +24,7 @@
      "[| !!m. P m 0;     \
 \        !!m n. [| 0<n;  P n (m mod n) |] ==> P m n  \
 \     |] ==> P (m::nat) (n::nat)";
-by (res_inst_tac [("u","m"),("v","n")] gcd.induct 1);
+by (induct_thm_tac gcd.induct "m n" 1);
 by (case_tac "n=0" 1);
 by (asm_simp_tac (simpset() addsimps prems) 1);
 by Safe_tac;
@@ -50,7 +50,7 @@
 
 (*gcd(m,n) divides m and n.  The conjunctions don't seem provable separately*)
 Goal "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)";
-by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
+by (induct_thm_tac gcd_induct "m n" 1);
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [gcd_non_0])));
 by (blast_tac (claset() addDs [dvd_mod_imp_dvd]) 1);
 qed "gcd_dvd_both";
@@ -62,7 +62,7 @@
 (*Maximality: for all m,n,f naturals, 
                 if f divides m and f divides n then f divides gcd(m,n)*)
 Goal "(f dvd m) --> (f dvd n) --> f dvd gcd(m,n)";
-by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
+by (induct_thm_tac gcd_induct "m n" 1);
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps[gcd_non_0, dvd_mod])));
 qed_spec_mp "gcd_greatest";
 
@@ -118,7 +118,7 @@
 
 (*Davenport, page 27*)
 Goal "k * gcd(m,n) = gcd(k*m, k*n)";
-by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
+by (induct_thm_tac gcd_induct "m n" 1);
 by (Asm_full_simp_tac 1);
 by (case_tac "k=0" 1);
  by (Asm_full_simp_tac 1);
diff -r 64b803edef39 -r 043098ba5098 src/HOL/ex/Primrec.ML
--- a/src/HOL/ex/Primrec.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/ex/Primrec.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -46,7 +46,7 @@
 
 (*PROPERTY A 4*)
 Goal "j < ack(i,j)";
-by (res_inst_tac [("u","i"),("v","j")] ack.induct 1);
+by (induct_thm_tac ack.induct "i j" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "less_ack2";
 
@@ -54,7 +54,7 @@
 
 (*PROPERTY A 5-, the single-step lemma*)
 Goal "ack(i,j) < ack(i, Suc(j))";
-by (res_inst_tac [("u","i"),("v","j")] ack.induct 1);
+by (induct_thm_tac ack.induct "i j" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "ack_less_ack_Suc2";
 
@@ -62,7 +62,7 @@
 
 (*PROPERTY A 5, monotonicity for < *)
 Goal "j<k --> ack(i,j) < ack(i,k)";
-by (res_inst_tac [("u","i"),("v","k")] ack.induct 1);
+by (induct_thm_tac ack.induct "i k" 1);
 by (ALLGOALS Asm_simp_tac);
 by (blast_tac (claset() addSEs [less_SucE] addIs [less_trans]) 1);
 qed_spec_mp "ack_less_mono2";
@@ -115,10 +115,10 @@
 
 (*PROPERTY A 7, monotonicity for < [not clear why ack_1 is now needed first!]*)
 Goal "ack(i,k) < ack(Suc(i+i'),k)";
-by (res_inst_tac [("u","i"),("v","k")] ack.induct 1);
+by (induct_thm_tac ack.induct "i k" 1);
 by (ALLGOALS Asm_full_simp_tac);
 by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 2);
-by (res_inst_tac [("u","i'"),("v","n")] ack.induct 1);
+by (induct_thm_tac ack.induct "i' n" 1);
 by (ALLGOALS Asm_simp_tac);
 by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 1);
 by (blast_tac (claset() addIs [Suc_leI RS le_less_trans, ack_less_mono2]) 1);
diff -r 64b803edef39 -r 043098ba5098 src/HOL/ex/Puzzle.ML
--- a/src/HOL/ex/Puzzle.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/ex/Puzzle.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -11,7 +11,7 @@
 AddSIs [Puzzle.f_ax];
 
 Goal "! n. k=f(n) --> n <= f(n)";
-by (res_inst_tac [("n","k")] less_induct 1);
+by (induct_thm_tac less_induct "k" 1);
 by (rtac allI 1);
 by (rename_tac "i" 1);
 by (case_tac "i" 1);
diff -r 64b803edef39 -r 043098ba5098 src/HOL/ex/Qsort.ML
--- a/src/HOL/ex/Qsort.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/ex/Qsort.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -9,7 +9,7 @@
 (*** Version one: higher-order ***)
 
 Goal "multiset (qsort(le,xs)) x = multiset xs x";
-by (res_inst_tac [("v","xs"),("u","le")] qsort.induct 1);
+by (induct_thm_tac qsort.induct "le xs" 1);
 by Auto_tac;
 qed "qsort_permutes";
 Addsimps [qsort_permutes];
@@ -21,7 +21,7 @@
 Addsimps [set_qsort];
 
 Goal "total(le) --> transf(le) --> sorted le (qsort(le,xs))";
-by (res_inst_tac [("v","xs"),("u","le")] qsort.induct 1);
+by (induct_thm_tac qsort.induct "le xs" 1);
 by (ALLGOALS Asm_simp_tac);
 by (rewrite_goals_tac [Sorting.total_def, Sorting.transf_def]);
 by (Blast_tac 1);
diff -r 64b803edef39 -r 043098ba5098 src/HOL/ex/Recdefs.ML
--- a/src/HOL/ex/Recdefs.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/ex/Recdefs.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -12,12 +12,12 @@
 Addsimps g.simps;
 
 Goal "g x < Suc x";
-by (res_inst_tac [("x","x")] g.induct 1);
+by (induct_thm_tac g.induct "x" 1);
 by Auto_tac;
 qed "g_terminates";
 
 Goal "g x = 0";
-by (res_inst_tac [("x","x")] g.induct 1);
+by (induct_thm_tac g.induct "x" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [g_terminates])));
 qed "g_zero";