# HG changeset patch
# User paulson
# Date 955631977 -7200
# Node ID 483a3eb96c7e5650a53a5a1c63c7d720f8e1e29d
# Parent  2f2d2b4215d60e07648716199bf386d4b0c96dd8
stopped using the obsolete "nat_ind_tac"

diff -r 2f2d2b4215d6 -r 483a3eb96c7e src/HOL/RelPow.ML
--- a/src/HOL/RelPow.ML	Thu Apr 13 15:18:02 2000 +0200
+++ b/src/HOL/RelPow.ML	Thu Apr 13 15:19:37 2000 +0200
@@ -21,7 +21,7 @@
 qed "rel_pow_Suc_I";
 
 Goal "!z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 by (Simp_tac  1);
 by (Asm_full_simp_tac 1);
 by (Blast_tac 1);
@@ -51,7 +51,7 @@
 qed "rel_pow_E";
 
 Goal "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 by (blast_tac (claset() addIs [rel_pow_0_I] 
 	                addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
 by (blast_tac (claset() addIs [rel_pow_Suc_I]  
@@ -60,7 +60,7 @@
 
 
 Goal "!x y z. (x,y) : R^n & (y,z) : R --> (? w. (x,w) : R & (w,z) : R^n)";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 by (ALLGOALS Asm_simp_tac);
 by (Blast_tac 1);
 qed_spec_mp "rel_pow_Suc_D2'";
@@ -89,7 +89,7 @@
 qed "rtrancl_imp_UN_rel_pow";
 
 Goal "!y. (x,y):R^n --> (x,y):R^*";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 by (blast_tac (claset() addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
 by (blast_tac (claset() addEs [rel_pow_Suc_E]
                        addIs [rtrancl_into_rtrancl]) 1);
diff -r 2f2d2b4215d6 -r 483a3eb96c7e src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Thu Apr 13 15:18:02 2000 +0200
+++ b/src/HOL/Univ.ML	Thu Apr 13 15:19:37 2000 +0200
@@ -214,7 +214,7 @@
 qed "ndepth_K0";
 
 Goal "k < Suc(LEAST x. f x = Inr 0) --> nat_case (Inr (Suc i)) f k ~= Inr 0";
-by (nat_ind_tac "k" 1);
+by (induct_tac "k" 1);
 by (ALLGOALS Simp_tac);
 by (rtac impI 1);
 by (etac not_less_Least 1);