author | wenzelm |
Thu, 27 Jun 2013 12:34:58 +0200 | |
changeset 52466 | a3b175675843 |
parent 52460 | 92ae850a9bfd (diff) |
parent 52465 | 4970437fe092 (current diff) |
child 52467 | 24c6ddb48cb8 |
--- 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*}