| changeset 45015 | fdac1e9880eb |
| parent 44890 | 22f665a2e91c |
| child 47818 | 151d137f1095 |
--- a/src/HOL/IMP/Hoare_Examples.thy Tue Sep 20 05:47:11 2011 +0200 +++ b/src/HOL/IMP/Hoare_Examples.thy Tue Sep 20 05:48:23 2011 +0200 @@ -25,7 +25,7 @@ lemma while_sum: "(w n, s) \<Rightarrow> t \<Longrightarrow> t ''x'' = s ''x'' + \<Sum> {s ''y'' + 1 .. n}" -apply(induct "w n" s t rule: big_step_induct) +apply(induction "w n" s t rule: big_step_induct) apply(auto simp add: setsum_head_plus_1) done