diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/AExp.thy
--- a/src/HOL/IMP/AExp.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/AExp.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -62,7 +62,7 @@
 
 theorem aval_asimp_const[simp]:
   "aval (asimp_const a) s = aval a s"
-apply(induct a)
+apply(induction a)
 apply (auto split: aexp.split)
 done
 
@@ -77,7 +77,7 @@
 
 lemma aval_plus[simp]:
   "aval (plus a1 a2) s = aval a1 s + aval a2 s"
-apply(induct a1 a2 rule: plus.induct)
+apply(induction a1 a2 rule: plus.induct)
 apply simp_all (* just for a change from auto *)
 done
 
@@ -94,7 +94,7 @@
 
 theorem aval_asimp[simp]:
   "aval (asimp a) s = aval a s"
-apply(induct a)
+apply(induction a)
 apply simp_all
 done