src/HOL/IMP/Small_Step.thy

--- a/src/HOL/IMP/Small_Step.thy	Tue Oct 22 16:07:09 2013 +0200
+++ b/src/HOL/IMP/Small_Step.thy	Wed Oct 23 09:58:30 2013 +0200
@@ -4,7 +4,6 @@
 
 subsection "The transition relation"
 
-text_raw{*\snip{SmallStepDef}{0}{2}{% *}
 inductive
   small_step :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>" 55)
 where
@@ -18,7 +17,6 @@
 
 While:   "(WHILE b DO c,s) \<rightarrow>
             (IF b THEN c;; WHILE b DO c ELSE SKIP,s)"
-text_raw{*}%endsnip*}
 
 
 abbreviation