Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authornipkow
Fri, 21 Oct 2011 17:39:07 +0200
changeset 45239 ccea94064585
parent 45237 769c4cbcd319 (current diff)
parent 45238 ed2bb3b58cc4 (diff)
child 45240 9d97bd3c086a
child 45246 4fbeabee6487
merged
--- 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)
isabelle