equal
deleted
inserted
replaced
30 by (induct xs arbitrary: n) (auto simp: algebra_simps) |
30 by (induct xs arbitrary: n) (auto simp: algebra_simps) |
31 |
31 |
32 subsection "Instructions and Stack Machine" |
32 subsection "Instructions and Stack Machine" |
33 |
33 |
34 datatype instr = |
34 datatype instr = |
35 LOADI int | |
35 LOADI int | |
36 LOAD string | |
36 LOAD vname | |
37 ADD | |
37 ADD | |
38 STORE string | |
38 STORE vname | |
39 JMP int | |
39 JMP int | |
40 JMPLESS int | |
40 JMPLESS int | |
41 JMPGE int |
41 JMPGE int |
42 |
42 |
43 type_synonym stack = "val list" |
43 type_synonym stack = "val list" |