diff -r 8ca612982014 -r bf39b07a7a8e src/HOL/IMP/Small_Step.thy
--- a/src/HOL/IMP/Small_Step.thy	Tue Nov 08 22:38:56 2011 +0100
+++ b/src/HOL/IMP/Small_Step.thy	Wed Nov 09 14:47:38 2011 +1100
@@ -4,6 +4,7 @@
 
 subsection "The transition relation"
 
+text_raw{*\begin{isaverbatimwrite}\newcommand{\SmallStepDef}{% *}
 inductive
   small_step :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>" 55)
 where
@@ -16,6 +17,7 @@
 IfFalse: "\<not>bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
 
 While:   "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
+text_raw{*}\end{isaverbatimwrite}*}
 
 
 abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)