# HG changeset patch
# User nipkow
# Date 1372320671 -7200
# Node ID 92ae850a9bfd79c39cbd27fc60e89661dcff04a1
# Parent  365ca7cb0d812adbb6d7b86913de6f8da6e058a4
tuned

diff -r 365ca7cb0d81 -r 92ae850a9bfd src/HOL/IMP/AExp.thy
--- 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*}