--- 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}{% *}
--- 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 *}
--- 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]