# HG changeset patch
# User kleing
# Date 1365940485 -36000
# Node ID 3d213f39d83c85ba2a61d59632f7ccd33a924d7d
# Parent  0b0fc7dc4ce4f77bb9d8e669b47d64f740d754b4
added another definition snipped

diff -r 0b0fc7dc4ce4 -r 3d213f39d83c src/HOL/IMP/Comp_Rev.thy
--- a/src/HOL/IMP/Comp_Rev.thy	Fri Apr 12 17:56:51 2013 +0200
+++ b/src/HOL/IMP/Comp_Rev.thy	Sun Apr 14 21:54:45 2013 +1000
@@ -17,12 +17,14 @@
   "P \<turnstile> c \<rightarrow>^(Suc n) c'' = (\<exists>c'. (P \<turnstile> c \<rightarrow> c') \<and> P \<turnstile> c' \<rightarrow>^n c'')"
 
 text {* The possible successor PCs of an instruction at position @{term n} *}
+text_raw{*\snip{isuccsdef}{0}{1}{% *}
 definition
   "isuccs i n \<equiv> case i of 
      JMP j \<Rightarrow> {n + 1 + j}
    | JMPLESS j \<Rightarrow> {n + 1 + j, n + 1}
    | JMPGE j \<Rightarrow> {n + 1 + j, n + 1}
    | _ \<Rightarrow> {n +1}"
+text_raw{*}%endsnip*}
 
 text {* The possible successors PCs of an instruction list *}
 definition