# HG changeset patch
# User nipkow
# Date 1319211540 -7200
# Node ID ed2bb3b58cc4319b184baf7b3262f775e92c8424
# Parent  62ca94616539dedbd941e8f1c7c1454d0d1bce74
tuned

diff -r 62ca94616539 -r ed2bb3b58cc4 src/HOL/IMP/AExp.thy
--- a/src/HOL/IMP/AExp.thy	Fri Oct 21 08:25:04 2011 +0200
+++ b/src/HOL/IMP/AExp.thy	Fri Oct 21 17:39:00 2011 +0200
@@ -60,7 +60,7 @@
     (N n1, N n2) \<Rightarrow> N(n1+n2) |
     (a1',a2') \<Rightarrow> Plus a1' a2')"
 
-theorem aval_asimp_const[simp]:
+theorem aval_asimp_const:
   "aval (asimp_const a) s = aval a s"
 apply(induction a)
 apply (auto split: aexp.split)