--- a/src/HOL/IMP/Compiler.thy Thu Aug 08 12:01:02 2013 +0200
+++ b/src/HOL/IMP/Compiler.thy Thu Aug 08 14:47:24 2013 +0200
@@ -34,14 +34,11 @@
subsection "Instructions and Stack Machine"
+text_raw{*\snip{instrdef}{0}{1}{% *}
datatype instr =
- LOADI int |
- LOAD vname |
- ADD |
- STORE vname |
- JMP int |
- JMPLESS int |
- JMPGE int
+ LOADI int | LOAD vname | ADD | STORE vname |
+ JMP int | JMPLESS int | JMPGE int
+text_raw{*}%endsnip*}
type_synonym stack = "val list"
type_synonym config = "int \<times> state \<times> stack"