1.1 --- a/src/HOL/IMP/Compiler.thy	Thu Aug 08 12:01:02 2013 +0200
     1.2 +++ b/src/HOL/IMP/Compiler.thy	Thu Aug 08 14:47:24 2013 +0200
     1.3 @@ -34,14 +34,11 @@
     1.4  
     1.5  subsection "Instructions and Stack Machine"
     1.6  
     1.7 +text_raw{*\snip{instrdef}{0}{1}{% *}
     1.8  datatype instr = 
     1.9 -  LOADI int |
    1.10 -  LOAD vname |
    1.11 -  ADD |
    1.12 -  STORE vname |
    1.13 -  JMP int |
    1.14 -  JMPLESS int |
    1.15 -  JMPGE int
    1.16 +  LOADI int | LOAD vname | ADD | STORE vname |
    1.17 +  JMP int | JMPLESS int | JMPGE int
    1.18 +text_raw{*}%endsnip*}
    1.19  
    1.20  type_synonym stack = "val list"
    1.21  type_synonym config = "int \<times> state \<times> stack"