
diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Def_Init.thy
--- a/src/HOL/IMP/Def_Init.thy	Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Def_Init.thy	Fri May 17 08:19:52 2013 +0200
@@ -7,7 +7,7 @@
 inductive D :: "vname set \<Rightarrow> com \<Rightarrow> vname set \<Rightarrow> bool" where
 Skip: "D A SKIP A" |
 Assign: "vars a \<subseteq> A \<Longrightarrow> D A (x ::= a) (insert x A)" |
-Seq: "\<lbrakk> D A\<^isub>1 c\<^isub>1 A\<^isub>2;  D A\<^isub>2 c\<^isub>2 A\<^isub>3 \<rbrakk> \<Longrightarrow> D A\<^isub>1 (c\<^isub>1; c\<^isub>2) A\<^isub>3" |
+Seq: "\<lbrakk> D A\<^isub>1 c\<^isub>1 A\<^isub>2;  D A\<^isub>2 c\<^isub>2 A\<^isub>3 \<rbrakk> \<Longrightarrow> D A\<^isub>1 (c\<^isub>1;; c\<^isub>2) A\<^isub>3" |
 If: "\<lbrakk> vars b \<subseteq> A;  D A c\<^isub>1 A\<^isub>1;  D A c\<^isub>2 A\<^isub>2 \<rbrakk> \<Longrightarrow>
   D A (IF b THEN c\<^isub>1 ELSE c\<^isub>2) (A\<^isub>1 Int A\<^isub>2)" |
 While: "\<lbrakk> vars b \<subseteq> A;  D A c A' \<rbrakk> \<Longrightarrow> D A (WHILE b DO c) A"
@@ -15,7 +15,7 @@
 inductive_cases [elim!]:
 "D A SKIP A'"
 "D A (x ::= a) A'"
-"D A (c1;c2) A'"
+"D A (c1;;c2) A'"
 "D A (IF b THEN c1 ELSE c2) A'"
 "D A (WHILE b DO c) A'"
 




