diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/Denotation.thy
--- a/src/HOL/IMP/Denotation.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Denotation.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -32,7 +32,7 @@
 text{* Equivalence of denotational and big-step semantics: *}
 
 lemma com1: "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> C(c)"
-apply (induct rule: big_step_induct)
+apply (induction rule: big_step_induct)
 apply auto
 (* while *)
 apply (unfold Gamma_def)
@@ -43,7 +43,7 @@
 done
 
 lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> (c,s) \<Rightarrow> t"
-apply (induct c arbitrary: s t)
+apply (induction c arbitrary: s t)
 apply auto 
 apply blast
 (* while *)