changeset 52660 | 7f7311d04727 |
parent 52506 | eb80a16a2b72 |
child 52731 | dacd47a0633f |
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Mon Jul 15 14:23:51 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Mon Jul 15 15:50:39 2013 +0200 @@ -426,7 +426,7 @@ fun mk_sumEN 1 = @{thm one_pointE} | mk_sumEN 2 = @{thm sumE} | mk_sumEN n = - (fold (fn i => fn thm => @{thm obj_sum_step} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF + (fold (fn i => fn thm => @{thm obj_sumE_f} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF replicate n (impI RS allI); fun mk_obj_sumEN_balanced n =