# HG changeset patch
# User nipkow
# Date 1510919958 -3600
# Node ID 02483f568c52455c7be8ca640ac69c4444f1f6bf
# Parent  6a85b8a9c28c89a1e43ecba003e8e40f060ec411
tuned

diff -r 6a85b8a9c28c -r 02483f568c52 src/HOL/IMP/ASM.thy
--- 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}{% *}