--- 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)