merged
authorwenzelm
Thu, 27 Jun 2013 12:34:58 +0200
changeset 52466 a3b175675843
parent 52460 92ae850a9bfd (diff)
parent 52465 4970437fe092 (current diff)
child 52467 24c6ddb48cb8
merged
--- a/src/HOL/IMP/AExp.thy	Thu Jun 27 11:33:42 2013 +0200
+++ b/src/HOL/IMP/AExp.thy	Thu Jun 27 12:34:58 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*}