tuned

--- a/src/HOL/IMP/AExp.thy	Wed Jun 26 22:18:06 2013 +0200
+++ b/src/HOL/IMP/AExp.thy	Thu Jun 27 10:11:11 2013 +0200
@@ -16,7 +16,7 @@
 fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
 "aval (N n) s = n" |
 "aval (V x) s = s x" |
-"aval (Plus a1 a2) s = aval a1 s + aval a2 s"
+"aval (Plus a\<^isub>1 a\<^isub>2) s = aval a\<^isub>1 s + aval a\<^isub>2 s"
 text_raw{*}%endsnip*}