src/HOLCF/FOCUS/Buffer_adm.ML
changeset 13454 01e2496dee05
parent 12484 7ad150f5fc10
child 13524 604d0f3622d6
     1.1 --- a/src/HOLCF/FOCUS/Buffer_adm.ML	Mon Aug 05 14:30:06 2002 +0200
     1.2 +++ b/src/HOLCF/FOCUS/Buffer_adm.ML	Mon Aug 05 14:32:56 2002 +0200
     1.3 @@ -112,7 +112,7 @@
     1.4  		\    (s,f\\<cdot>s):down_iterate BufAC_Cmt_F i";
     1.5  by (res_inst_tac [("x","%i. 2*i")] exI 1);
     1.6  by (rtac allI 1);
     1.7 -by (nat_ind_tac "i" 1);
     1.8 +by (induct_tac "i" 1);
     1.9  by ( Simp_tac 1);
    1.10  by (simp_tac (simpset() addsimps [add_commute]) 1);
    1.11  by (strip_tac 1);