--- a/src/HOL/IMP/Small_Step.thy Tue Aug 13 14:20:22 2013 +0200
+++ b/src/HOL/IMP/Small_Step.thy Tue Aug 13 16:25:47 2013 +0200
@@ -10,11 +10,11 @@
where
Assign: "(x ::= a, s) \<rightarrow> (SKIP, s(x := aval a s))" |
-Seq1: "(SKIP;;c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
-Seq2: "(c\<^isub>1,s) \<rightarrow> (c\<^isub>1',s') \<Longrightarrow> (c\<^isub>1;;c\<^isub>2,s) \<rightarrow> (c\<^isub>1';;c\<^isub>2,s')" |
+Seq1: "(SKIP;;c\<^sub>2,s) \<rightarrow> (c\<^sub>2,s)" |
+Seq2: "(c\<^sub>1,s) \<rightarrow> (c\<^sub>1',s') \<Longrightarrow> (c\<^sub>1;;c\<^sub>2,s) \<rightarrow> (c\<^sub>1';;c\<^sub>2,s')" |
-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)" |
+IfTrue: "bval b s \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2,s) \<rightarrow> (c\<^sub>1,s)" |
+IfFalse: "\<not>bval b s \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2,s) \<rightarrow> (c\<^sub>2,s)" |
While: "(WHILE b DO c,s) \<rightarrow>
(IF b THEN c;; WHILE b DO c ELSE SKIP,s)"