changeset 8709 | 483a3eb96c7e |
parent 8703 | 816d8f6513be |
child 8790 | c4aaa5936e0c |
--- 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);