| changeset 20898 | 113c9516a2d7 |
| parent 20848 | 27a09c3eca1f |
| child 21404 | eb85850d3eb7 |
--- a/src/HOL/Hyperreal/HSeries.thy Mon Oct 09 02:19:49 2006 +0200 +++ b/src/HOL/Hyperreal/HSeries.thy Mon Oct 09 02:19:51 2006 +0200 @@ -83,7 +83,7 @@ done lemma sumhr_split_diff: "n<p ==> sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)" -by (drule_tac f1 = f in sumhr_split_add [symmetric], simp) +by (drule_tac f = f in sumhr_split_add [symmetric], simp) lemma sumhr_hrabs: "abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))" apply (cases n, cases m)