# HG changeset patch
# User nipkow
# Date 1352742169 -3600
# Node ID 6da283e4497b9540a7410d43575fbfadcd4b0b8e
# Parent  fea589c8583e5a870c702553b152c727cc0fe78a
tuned layout

diff -r fea589c8583e -r 6da283e4497b src/HOL/IMP/Big_Step.thy
--- a/src/HOL/IMP/Big_Step.thy	Mon Nov 12 14:46:42 2012 +0100
+++ b/src/HOL/IMP/Big_Step.thy	Mon Nov 12 18:42:49 2012 +0100
@@ -14,13 +14,13 @@
           (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
 
 IfTrue:  "\<lbrakk> bval b s;  (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
-         (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
+          (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
 IfFalse: "\<lbrakk> \<not>bval b s;  (c\<^isub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
-         (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
+          (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
 
 WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s" |
 WhileTrue:  "\<lbrakk> bval b s\<^isub>1;  (c,s\<^isub>1) \<Rightarrow> s\<^isub>2;  (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
-             (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3"
+                (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3"
 text_raw{*}%endsnip*}
 
 text_raw{*\snip{BigStepEx}{1}{2}{% *}
diff -r fea589c8583e -r 6da283e4497b src/HOL/IMP/Small_Step.thy
--- 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 *}
diff -r fea589c8583e -r 6da283e4497b src/HOL/IMP/Star.thy
--- a/src/HOL/IMP/Star.thy	Mon Nov 12 14:46:42 2012 +0100
+++ b/src/HOL/IMP/Star.thy	Mon Nov 12 18:42:49 2012 +0100
@@ -17,7 +17,8 @@
   case step thus ?case by (metis star.step)
 qed
 
-lemmas star_induct = star.induct[of "r:: 'a*'b \<Rightarrow> 'a*'b \<Rightarrow> bool", split_format(complete)]
+lemmas star_induct =
+  star.induct[of "r:: 'a*'b \<Rightarrow> 'a*'b \<Rightarrow> bool", split_format(complete)]
 
 declare star.refl[simp,intro]