# HG changeset patch
# User kleing
# Date 1364483508 -3600
# Node ID acc4bd79e2e97d880bf6a9448c1398dfa747d21a
# Parent  6d3a3ea5fc6e9fed4b8a301ddd0198464f92902e
replace induction by hammer

diff -r 6d3a3ea5fc6e -r acc4bd79e2e9 src/HOL/IMP/Fold.thy
--- a/src/HOL/IMP/Fold.thy	Thu Mar 28 15:47:03 2013 +0100
+++ b/src/HOL/IMP/Fold.thy	Thu Mar 28 16:11:48 2013 +0100
@@ -25,9 +25,7 @@
 theorem aval_afold_N:
 assumes "approx t s"
 shows "afold a t = N n \<Longrightarrow> aval a s = n"
-  using assms
-  by (induct a arbitrary: n)
-     (auto simp: approx_def split: aexp.splits option.splits)
+  by (metis assms aval.simps(1) aval_afold)
 
 definition
   "merge t1 t2 = (\<lambda>m. if t1 m = t2 m then t1 m else None)"