diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/Hoare_Examples.thy
--- 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