--- a/src/HOL/IMP/ASM.thy Thu Nov 16 11:30:23 2017 +0100
+++ b/src/HOL/IMP/ASM.thy Fri Nov 17 12:59:18 2017 +0100
@@ -12,9 +12,6 @@
type_synonym stack = "val list"
text_raw{*}%endsnip*}
-abbreviation "hd2 xs == hd(tl xs)"
-abbreviation "tl2 xs == tl(tl xs)"
-
text{* \noindent Abbreviations are transparent: they are unfolded after
parsing and folded back again before printing. Internally, they do not
exist.*}
@@ -23,7 +20,7 @@
fun exec1 :: "instr \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
"exec1 (LOADI n) _ stk = n # stk" |
"exec1 (LOAD x) s stk = s(x) # stk" |
-"exec1 ADD _ stk = (hd2 stk + hd stk) # tl2 stk"
+"exec1 ADD _ (j # i # stk) = (i + j) # stk"
text_raw{*}%endsnip*}
text_raw{*\snip{ASMexecdef}{1}{2}{% *}