Simprocs for type "nat" no longer introduce numerals unless
authorpaulson
Mon Jun 25 15:36:55 2001 +0200 (2001-06-25)
changeset 113785c84a5ca3a21
parent 11377 0f16ad464c62
child 11379 0c90ffd3f3e2
Simprocs for type "nat" no longer introduce numerals unless
src/HOLCF/FOCUS/Buffer_adm.ML
     1.1 --- a/src/HOLCF/FOCUS/Buffer_adm.ML	Mon Jun 25 15:35:59 2001 +0200
     1.2 +++ b/src/HOLCF/FOCUS/Buffer_adm.ML	Mon Jun 25 15:36:55 2001 +0200
     1.3 @@ -110,7 +110,7 @@
     1.4  Goal "f:BufEq ==> ? l. !i x s. s:BufAC_Asm --> x << s --> Fin (l i) < #x --> \
     1.5  		\    (x,f\\<cdot>x):down_iterate BufAC_Cmt_F i --> \
     1.6  		\    (s,f\\<cdot>s):down_iterate BufAC_Cmt_F i";
     1.7 -by (res_inst_tac [("x","%i. i+i")] exI 1);
     1.8 +by (res_inst_tac [("x","%i. #2*i")] exI 1);
     1.9  by (rtac allI 1);
    1.10  by (nat_ind_tac "i" 1);
    1.11  by ( Simp_tac 1);