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