Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Hoare_Parallel/OG_Tran.thy
changeset 32960 69916a850301
parent 32621 a073cb249a06
child 35107 bdca9f765ee4 
--- a/src/HOL/Hoare_Parallel/OG_Tran.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Tran.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -51,7 +51,7 @@
                          (Some (AnnSeq c (AnnWhile i b i c)), s)"
 
 | AnnAwait: "\<lbrakk> s \<in> b; atom_com c; (c, s) -P*\<rightarrow> (Parallel [], t) \<rbrakk> \<Longrightarrow>
-	           (Some (AnnAwait r b c), s) -1\<rightarrow> (None, t)" 
+                   (Some (AnnAwait r b c), s) -1\<rightarrow> (None, t)" 
 
 | Parallel: "\<lbrakk> i<length Ts; Ts!i = (Some c, q); (Some c, s) -1\<rightarrow> (r, t) \<rbrakk>
               \<Longrightarrow> (Parallel Ts, s) -P1\<rightarrow> (Parallel (Ts [i:=(r, q)]), t)"
isabelle