author | nipkow |
Thu, 27 Oct 2011 15:59:33 +0200 | |
changeset 45276 | cd0f6643e998 |
parent 45274 | 252cd58847e0 (current diff) |
parent 45275 | 7f6c2db48b71 (diff) |
child 45277 | 85b0ca9dd82f |
--- 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''))"