src/HOL/IMP/AExp.thy

     (N n1, N n2) \<Rightarrow> N(n1+n2) |
     (a1',a2') \<Rightarrow> Plus a1' a2')"
 
 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
 
 text{* Now we also eliminate all occurrences 0 in additions. The standard
 method: optimized versions of the constructors: *}

 "plus a (N i) = (if i=0 then a else Plus a (N i))" |
 "plus a1 a2 = Plus a1 a2"
 
 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
 
 fun asimp :: "aexp \<Rightarrow> aexp" where
 "asimp (N n) = N n" |

 
 value "asimp (Plus (Plus (N 0) (N 0)) (Plus (V ''x'') (N 0)))"
 
 theorem aval_asimp[simp]:
   "aval (asimp a) s = aval a s"
-apply(induct a)
+apply(induction a)
 apply simp_all
 done
 
 end