tuned
authornipkow
Fri Nov 17 12:59:18 2017 +0100 (17 months ago)
changeset 6707902483f568c52
parent 67078 6a85b8a9c28c
child 67080 2c0f24e927dd
tuned
src/HOL/IMP/ASM.thy
     1.1 --- a/src/HOL/IMP/ASM.thy	Thu Nov 16 11:30:23 2017 +0100
     1.2 +++ b/src/HOL/IMP/ASM.thy	Fri Nov 17 12:59:18 2017 +0100
     1.3 @@ -12,9 +12,6 @@
     1.4  type_synonym stack = "val list"
     1.5  text_raw{*}%endsnip*}
     1.6  
     1.7 -abbreviation "hd2 xs == hd(tl xs)"
     1.8 -abbreviation "tl2 xs == tl(tl xs)"
     1.9 -
    1.10  text{* \noindent Abbreviations are transparent: they are unfolded after
    1.11  parsing and folded back again before printing. Internally, they do not
    1.12  exist.*}
    1.13 @@ -23,7 +20,7 @@
    1.14  fun exec1 :: "instr \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
    1.15  "exec1 (LOADI n) _ stk  =  n # stk" |
    1.16  "exec1 (LOAD x) s stk  =  s(x) # stk" |
    1.17 -"exec1  ADD _ stk  =  (hd2 stk + hd stk) # tl2 stk"
    1.18 +"exec1  ADD _ (j # i # stk)  =  (i + j) # stk"
    1.19  text_raw{*}%endsnip*}
    1.20  
    1.21  text_raw{*\snip{ASMexecdef}{1}{2}{% *}