src/HOL/IMP/Procs_Stat_Vars_Dyn.thy
changeset 47818 151d137f1095
parent 45212 e87feee00a4c
child 51019 146f63c3f024
--- a/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy	Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy	Sat Apr 28 07:38:22 2012 +0200
@@ -10,7 +10,7 @@
 where
 Skip:    "pe \<turnstile> (SKIP,s) \<Rightarrow> s" |
 Assign:  "pe \<turnstile> (x ::= a,s) \<Rightarrow> s(x := aval a s)" |
-Semi:    "\<lbrakk> pe \<turnstile> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2;  pe \<turnstile> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
+Seq:     "\<lbrakk> pe \<turnstile> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2;  pe \<turnstile> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
           pe \<turnstile> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
 
 IfTrue:  "\<lbrakk> bval b s;  pe \<turnstile> (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>