# HG changeset patch
# User nipkow
# Date 1319723973 -7200
# Node ID cd0f6643e9982ced7f58b2b59b14f294e05a7a73
# Parent  252cd58847e031fdb717811cde24e319eb11fc8d# Parent  7f6c2db48b71bd2a3c73f0c34dc00595dc38fa09
merged

diff -r 252cd58847e0 -r cd0f6643e998 src/HOL/IMP/ASM.thy
--- a/src/HOL/IMP/ASM.thy	Thu Oct 27 13:52:31 2011 +0200
+++ b/src/HOL/IMP/ASM.thy	Thu Oct 27 15:59:33 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''))"