# HG changeset patch
# User nipkow
# Date 1319211547 -7200
# Node ID ccea94064585691193c11fd884ed5ebd2f9106fd
# Parent  769c4cbcd319effdce2b312c07cbf7e99a6911f7# Parent  ed2bb3b58cc4319b184baf7b3262f775e92c8424
merged

diff -r 769c4cbcd319 -r ccea94064585 src/HOL/IMP/AExp.thy
--- a/src/HOL/IMP/AExp.thy	Fri Oct 21 16:21:12 2011 +0200
+++ b/src/HOL/IMP/AExp.thy	Fri Oct 21 17:39:07 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)