--- a/src/HOL/IMP/Small_Step.thy Mon Nov 12 14:46:42 2012 +0100
+++ b/src/HOL/IMP/Small_Step.thy Mon Nov 12 18:42:49 2012 +0100
@@ -16,11 +16,13 @@
IfTrue: "bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" |
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)"
+While: "(WHILE b DO c,s) \<rightarrow>
+ (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
text_raw{*}%endsnip*}
-abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
+abbreviation
+ small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
where "x \<rightarrow>* y == star small_step x y"
subsection{* Executability *}