# HG changeset patch
# User nipkow
# Date 1319723965 -7200
# Node ID 7f6c2db48b71bd2a3c73f0c34dc00595dc38fa09
# Parent  66823a0066db163da40563371c0710970988c514
tuned text

diff -r 66823a0066db -r 7f6c2db48b71 src/HOL/IMP/ASM.thy
--- a/src/HOL/IMP/ASM.thy	Tue Oct 25 16:37:11 2011 +0200
+++ b/src/HOL/IMP/ASM.thy	Thu Oct 27 15:59:25 2011 +0200
@@ -48,7 +48,7 @@
 fun comp :: "aexp \<Rightarrow> instr list" where
 "comp (N n) = [LOADI n]" |
 "comp (V x) = [LOAD x]" |
-"comp (Plus e1 e2) = comp e1 @ comp e2 @ [ADD]"
+"comp (Plus e\<^isub>1 e\<^isub>2) = comp e\<^isub>1 @ comp e\<^isub>2 @ [ADD]"
 text_raw{*}\end{isaverbatimwrite}*}
 
 value "comp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"