src/HOL/Induct/LList.ML
changeset 9870 2374ba026fc6
parent 9747 043098ba5098
child 10186 499637e8f2c6
     1.1 --- a/src/HOL/Induct/LList.ML	Tue Sep 05 21:06:01 2000 +0200
     1.2 +++ b/src/HOL/Induct/LList.ML	Wed Sep 06 08:04:41 2000 +0200
     1.3 @@ -128,7 +128,7 @@
     1.4  qed "LListD_unfold";
     1.5  
     1.6  Goal "!M N. (M,N) : LListD(diag A) --> ntrunc k M = ntrunc k N";
     1.7 -by (induct_thm_tac less_induct "k" 1);
     1.8 +by (induct_thm_tac nat_less_induct "k" 1);
     1.9  by (safe_tac (claset() delrules [equalityI]));
    1.10  by (etac LListD.elim 1);
    1.11  by (safe_tac (claset() delrules [equalityI]));
    1.12 @@ -287,7 +287,7 @@
    1.13  by (rtac (ntrunc_equality RS ext) 1);
    1.14  by (rename_tac "x k" 1);
    1.15  by (res_inst_tac [("x", "x")] spec 1);
    1.16 -by (induct_thm_tac less_induct "k" 1);
    1.17 +by (induct_thm_tac nat_less_induct "k" 1);
    1.18  by (rename_tac "n" 1);
    1.19  by (rtac allI 1);
    1.20  by (rename_tac "y" 1);