# HG changeset patch
# User wenzelm
# Date 1377641930 -7200
# Node ID effd8fcabca29cb61698c6797b696e4842040472
# Parent  07593a0a27f471b5bb6ee19fcb27ee6fedf73e61
more symbols;

diff -r 07593a0a27f4 -r effd8fcabca2 src/HOL/Hoare_Parallel/Gar_Coll.thy
--- a/src/HOL/Hoare_Parallel/Gar_Coll.thy	Tue Aug 27 23:54:23 2013 +0200
+++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy	Wed Aug 28 00:18:50 2013 +0200
@@ -40,15 +40,15 @@
 edge but has not yet colored the new target.   *}
 
 definition Redirect_Edge :: "gar_coll_state ann_com" where
-  "Redirect_Edge \<equiv> .{\<acute>Mut_init \<and> \<acute>z}. \<langle>\<acute>E:=\<acute>E[R:=(fst(\<acute>E!R), T)],, \<acute>z:= (\<not>\<acute>z)\<rangle>"
+  "Redirect_Edge \<equiv> \<lbrace>\<acute>Mut_init \<and> \<acute>z\<rbrace> \<langle>\<acute>E:=\<acute>E[R:=(fst(\<acute>E!R), T)],, \<acute>z:= (\<not>\<acute>z)\<rangle>"
 
 definition Color_Target :: "gar_coll_state ann_com" where
-  "Color_Target \<equiv> .{\<acute>Mut_init \<and> \<not>\<acute>z}. \<langle>\<acute>M:=\<acute>M[T:=Black],, \<acute>z:= (\<not>\<acute>z)\<rangle>"
+  "Color_Target \<equiv> \<lbrace>\<acute>Mut_init \<and> \<not>\<acute>z\<rbrace> \<langle>\<acute>M:=\<acute>M[T:=Black],, \<acute>z:= (\<not>\<acute>z)\<rangle>"
 
 definition Mutator :: "gar_coll_state ann_com" where
   "Mutator \<equiv>
-  .{\<acute>Mut_init \<and> \<acute>z}. 
-  WHILE True INV .{\<acute>Mut_init \<and> \<acute>z}. 
+  \<lbrace>\<acute>Mut_init \<and> \<acute>z\<rbrace> 
+  WHILE True INV \<lbrace>\<acute>Mut_init \<and> \<acute>z\<rbrace> 
   DO  Redirect_Edge ;; Color_Target  OD"
 
 subsubsection {* Correctness of the mutator *}
@@ -64,14 +64,14 @@
 done
 
 lemma Color_Target:
-  "\<turnstile> Color_Target .{\<acute>Mut_init \<and> \<acute>z}."
+  "\<turnstile> Color_Target \<lbrace>\<acute>Mut_init \<and> \<acute>z\<rbrace>"
 apply (unfold mutator_defs)
 apply annhoare
 apply(simp_all)
 done
 
 lemma Mutator: 
- "\<turnstile> Mutator .{False}."
+ "\<turnstile> Mutator \<lbrace>False\<rbrace>"
 apply(unfold Mutator_def)
 apply annhoare
 apply(simp_all add:Redirect_Edge Color_Target)
@@ -101,21 +101,21 @@
 
 definition Blacken_Roots :: " gar_coll_state ann_com" where
   "Blacken_Roots \<equiv> 
-  .{\<acute>Proper}.
+  \<lbrace>\<acute>Proper\<rbrace>
   \<acute>ind:=0;;
-  .{\<acute>Proper \<and> \<acute>ind=0}.
+  \<lbrace>\<acute>Proper \<and> \<acute>ind=0\<rbrace>
   WHILE \<acute>ind<length \<acute>M 
-   INV .{\<acute>Proper \<and> (\<forall>i<\<acute>ind. i \<in> Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind\<le>length \<acute>M}.
-  DO .{\<acute>Proper \<and> (\<forall>i<\<acute>ind. i \<in> Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M}.
+   INV \<lbrace>\<acute>Proper \<and> (\<forall>i<\<acute>ind. i \<in> Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind\<le>length \<acute>M\<rbrace>
+  DO \<lbrace>\<acute>Proper \<and> (\<forall>i<\<acute>ind. i \<in> Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M\<rbrace>
    IF \<acute>ind\<in>Roots THEN 
-   .{\<acute>Proper \<and> (\<forall>i<\<acute>ind. i \<in> Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M \<and> \<acute>ind\<in>Roots}. 
+   \<lbrace>\<acute>Proper \<and> (\<forall>i<\<acute>ind. i \<in> Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M \<and> \<acute>ind\<in>Roots\<rbrace> 
     \<acute>M:=\<acute>M[\<acute>ind:=Black] FI;;
-   .{\<acute>Proper \<and> (\<forall>i<\<acute>ind+1. i \<in> Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M}.
+   \<lbrace>\<acute>Proper \<and> (\<forall>i<\<acute>ind+1. i \<in> Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M\<rbrace>
     \<acute>ind:=\<acute>ind+1 
   OD"
 
 lemma Blacken_Roots: 
- "\<turnstile> Blacken_Roots .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M}."
+ "\<turnstile> Blacken_Roots \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M\<rbrace>"
 apply (unfold Blacken_Roots_def)
 apply annhoare
 apply(simp_all add:collector_defs Graph_defs)
@@ -135,28 +135,28 @@
 
 definition Propagate_Black_aux :: "gar_coll_state ann_com" where
   "Propagate_Black_aux \<equiv>
-  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M}.
+  \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M\<rbrace>
   \<acute>ind:=0;;
-  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> \<acute>ind=0}. 
+  \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> \<acute>ind=0\<rbrace> 
   WHILE \<acute>ind<length \<acute>E 
-   INV .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
-         \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>E}.
-  DO .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
-       \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E}. 
+   INV \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
+         \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>E\<rbrace>
+  DO \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
+       \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E\<rbrace> 
    IF \<acute>M!(fst (\<acute>E!\<acute>ind)) = Black THEN 
-    .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
-       \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E \<and> \<acute>M!fst(\<acute>E!\<acute>ind)=Black}.
+    \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
+       \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E \<and> \<acute>M!fst(\<acute>E!\<acute>ind)=Black\<rbrace>
      \<acute>M:=\<acute>M[snd(\<acute>E!\<acute>ind):=Black];;
-    .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
-       \<and> \<acute>PBInv (\<acute>ind + 1) \<and> \<acute>ind<length \<acute>E}.
+    \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
+       \<and> \<acute>PBInv (\<acute>ind + 1) \<and> \<acute>ind<length \<acute>E\<rbrace>
      \<acute>ind:=\<acute>ind+1
    FI
   OD"
 
 lemma Propagate_Black_aux: 
   "\<turnstile>  Propagate_Black_aux
-  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
-    \<and> ( \<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)}."
+  \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
+    \<and> ( \<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)\<rbrace>"
 apply (unfold Propagate_Black_aux_def  PBInv_def collector_defs)
 apply annhoare
 apply(simp_all add:Graph6 Graph7 Graph8 Graph12)
@@ -215,32 +215,32 @@
 
 definition Propagate_Black :: " gar_coll_state ann_com" where
   "Propagate_Black \<equiv>
-  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M}.
+  \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M\<rbrace>
   \<acute>ind:=0;;
-  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> \<acute>ind=0}.
+  \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> \<acute>ind=0\<rbrace>
   WHILE \<acute>ind<length \<acute>E 
-   INV .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
-         \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>E}.
-  DO .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
-       \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E}. 
+   INV \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
+         \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>E\<rbrace>
+  DO \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
+       \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E\<rbrace> 
    IF (\<acute>M!(fst (\<acute>E!\<acute>ind)))=Black THEN 
-    .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
-      \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E \<and> (\<acute>M!fst(\<acute>E!\<acute>ind))=Black}.
+    \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
+      \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E \<and> (\<acute>M!fst(\<acute>E!\<acute>ind))=Black\<rbrace>
      \<acute>k:=(snd(\<acute>E!\<acute>ind));;
-    .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
+    \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
       \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E \<and> (\<acute>M!fst(\<acute>E!\<acute>ind))=Black 
-      \<and> \<acute>Auxk}.
+      \<and> \<acute>Auxk\<rbrace>
      \<langle>\<acute>M:=\<acute>M[\<acute>k:=Black],, \<acute>ind:=\<acute>ind+1\<rangle>
-   ELSE .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
-          \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E}. 
+   ELSE \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
+          \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E\<rbrace> 
          \<langle>IF (\<acute>M!(fst (\<acute>E!\<acute>ind)))\<noteq>Black THEN \<acute>ind:=\<acute>ind+1 FI\<rangle> 
    FI
   OD"
 
 lemma Propagate_Black: 
   "\<turnstile>  Propagate_Black
-  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
-    \<and> ( \<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)}."
+  \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
+    \<and> ( \<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)\<rbrace>"
 apply (unfold Propagate_Black_def  PBInv_def Auxk_def collector_defs)
 apply annhoare
 apply(simp_all add: Graph6 Graph7 Graph8 Graph12)
@@ -325,42 +325,42 @@
 
 definition Count :: " gar_coll_state ann_com" where
   "Count \<equiv>
-  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M 
+  \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M 
     \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
-    \<and> length \<acute>Ma=length \<acute>M \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>bc={}}.
+    \<and> length \<acute>Ma=length \<acute>M \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>bc={}\<rbrace>
   \<acute>ind:=0;;
-  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M 
+  \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M 
     \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
    \<and> length \<acute>Ma=length \<acute>M \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>bc={} 
-   \<and> \<acute>ind=0}.
+   \<and> \<acute>ind=0\<rbrace>
    WHILE \<acute>ind<length \<acute>M 
-     INV .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M 
+     INV \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M 
            \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
            \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv \<acute>ind
-           \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind\<le>length \<acute>M}.
-   DO .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M 
+           \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind\<le>length \<acute>M\<rbrace>
+   DO \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M 
          \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
          \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv \<acute>ind 
-         \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind<length \<acute>M}. 
+         \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind<length \<acute>M\<rbrace> 
        IF \<acute>M!\<acute>ind=Black 
-          THEN .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M 
+          THEN \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M 
                  \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
                  \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv \<acute>ind
-                 \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black}.
+                 \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black\<rbrace>
           \<acute>bc:=insert \<acute>ind \<acute>bc
        FI;;
-      .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M 
+      \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M 
         \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
         \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv (\<acute>ind+1)
-        \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind<length \<acute>M}.
+        \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind<length \<acute>M\<rbrace>
       \<acute>ind:=\<acute>ind+1
    OD"
 
 lemma Count: 
   "\<turnstile> Count 
-  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M 
+  \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M 
    \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> length \<acute>Ma=length \<acute>M
-   \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe)}."
+   \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe)\<rbrace>"
 apply(unfold Count_def)
 apply annhoare
 apply(simp_all add:CountInv_def Graph6 Graph7 Graph8 Graph12 Blacks_def collector_defs)
@@ -392,24 +392,24 @@
 
 definition Append :: "gar_coll_state ann_com" where
    "Append \<equiv>
-  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe}.
+  \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe\<rbrace>
   \<acute>ind:=0;;
-  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe \<and> \<acute>ind=0}.
+  \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe \<and> \<acute>ind=0\<rbrace>
     WHILE \<acute>ind<length \<acute>M 
-      INV .{\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>M}.
-    DO .{\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M}.
+      INV \<lbrace>\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>M\<rbrace>
+    DO \<lbrace>\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M\<rbrace>
        IF \<acute>M!\<acute>ind=Black THEN 
-          .{\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black}. 
+          \<lbrace>\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black\<rbrace> 
           \<acute>M:=\<acute>M[\<acute>ind:=White] 
-       ELSE .{\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>ind\<notin>Reach \<acute>E}.
+       ELSE \<lbrace>\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>ind\<notin>Reach \<acute>E\<rbrace>
               \<acute>E:=Append_to_free(\<acute>ind,\<acute>E)
        FI;;
-     .{\<acute>Proper \<and> \<acute>AppendInv (\<acute>ind+1) \<and> \<acute>ind<length \<acute>M}. 
+     \<lbrace>\<acute>Proper \<and> \<acute>AppendInv (\<acute>ind+1) \<and> \<acute>ind<length \<acute>M\<rbrace> 
        \<acute>ind:=\<acute>ind+1
     OD"
 
 lemma Append: 
-  "\<turnstile> Append .{\<acute>Proper}."
+  "\<turnstile> Append \<lbrace>\<acute>Proper\<rbrace>"
 apply(unfold Append_def AppendInv_def)
 apply annhoare
 apply(simp_all add:collector_defs Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
@@ -433,30 +433,30 @@
 
 definition Collector :: " gar_coll_state ann_com" where
   "Collector \<equiv>
-.{\<acute>Proper}.  
- WHILE True INV .{\<acute>Proper}. 
+\<lbrace>\<acute>Proper\<rbrace>  
+ WHILE True INV \<lbrace>\<acute>Proper\<rbrace> 
  DO  
   Blacken_Roots;; 
-  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M}.  
+  \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M\<rbrace>  
    \<acute>obc:={};; 
-  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={}}. 
+  \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={}\<rbrace> 
    \<acute>bc:=Roots;; 
-  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots}. 
+  \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots\<rbrace> 
    \<acute>Ma:=M_init;;  
-  .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots \<and> \<acute>Ma=M_init}. 
+  \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots \<and> \<acute>Ma=M_init\<rbrace> 
    WHILE \<acute>obc\<noteq>\<acute>bc  
-     INV .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M 
+     INV \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M 
            \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
-           \<and> length \<acute>Ma=length \<acute>M \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe)}. 
-   DO .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M}.
+           \<and> length \<acute>Ma=length \<acute>M \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe)\<rbrace> 
+   DO \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M\<rbrace>
        \<acute>obc:=\<acute>bc;;
        Propagate_Black;; 
-      .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
-        \<and> (\<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)}. 
+      \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
+        \<and> (\<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)\<rbrace> 
        \<acute>Ma:=\<acute>M;;
-      .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma 
+      \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma 
         \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> length \<acute>Ma=length \<acute>M 
-        \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe)}.
+        \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe)\<rbrace>
        \<acute>bc:={};;
        Count 
    OD;; 
@@ -464,7 +464,7 @@
  OD"
 
 lemma Collector: 
-  "\<turnstile> Collector .{False}."
+  "\<turnstile> Collector \<lbrace>False\<rbrace>"
 apply(unfold Collector_def)
 apply annhoare
 apply(simp_all add: Blacken_Roots Propagate_Black Count Append)
@@ -806,15 +806,15 @@
 text {* In total there are 289 verification conditions.  *}
 
 lemma Gar_Coll: 
-  "\<parallel>- .{\<acute>Proper \<and> \<acute>Mut_init \<and> \<acute>z}.  
+  "\<parallel>- \<lbrace>\<acute>Proper \<and> \<acute>Mut_init \<and> \<acute>z\<rbrace>  
   COBEGIN  
    Collector
-  .{False}.
+  \<lbrace>False\<rbrace>
  \<parallel>  
    Mutator
-  .{False}. 
+  \<lbrace>False\<rbrace> 
  COEND 
-  .{False}."
+  \<lbrace>False\<rbrace>"
 apply oghoare
 apply(force simp add: Mutator_def Collector_def modules)
 apply(rule Collector)
diff -r 07593a0a27f4 -r effd8fcabca2 src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy
--- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Tue Aug 27 23:54:23 2013 +0200
+++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Wed Aug 28 00:18:50 2013 +0200
@@ -32,21 +32,21 @@
 
 definition Mul_Redirect_Edge  :: "nat \<Rightarrow> nat \<Rightarrow> mul_gar_coll_state ann_com" where
   "Mul_Redirect_Edge j n \<equiv>
-  .{\<acute>Mul_mut_init n \<and> Z (\<acute>Muts!j)}.
+  \<lbrace>\<acute>Mul_mut_init n \<and> Z (\<acute>Muts!j)\<rbrace>
   \<langle>IF T(\<acute>Muts!j) \<in> Reach \<acute>E THEN  
   \<acute>E:= \<acute>E[R (\<acute>Muts!j):= (fst (\<acute>E!R(\<acute>Muts!j)), T (\<acute>Muts!j))] FI,, 
   \<acute>Muts:= \<acute>Muts[j:= (\<acute>Muts!j) \<lparr>Z:=False\<rparr>]\<rangle>"
 
 definition Mul_Color_Target :: "nat \<Rightarrow> nat \<Rightarrow> mul_gar_coll_state ann_com" where
   "Mul_Color_Target j n \<equiv>
-  .{\<acute>Mul_mut_init n \<and> \<not> Z (\<acute>Muts!j)}. 
+  \<lbrace>\<acute>Mul_mut_init n \<and> \<not> Z (\<acute>Muts!j)\<rbrace> 
   \<langle>\<acute>M:=\<acute>M[T (\<acute>Muts!j):=Black],, \<acute>Muts:=\<acute>Muts[j:= (\<acute>Muts!j) \<lparr>Z:=True\<rparr>]\<rangle>"
 
 definition Mul_Mutator :: "nat \<Rightarrow> nat \<Rightarrow>  mul_gar_coll_state ann_com" where
   "Mul_Mutator j n \<equiv>
-  .{\<acute>Mul_mut_init n \<and> Z (\<acute>Muts!j)}.  
+  \<lbrace>\<acute>Mul_mut_init n \<and> Z (\<acute>Muts!j)\<rbrace>  
   WHILE True  
-    INV .{\<acute>Mul_mut_init n \<and> Z (\<acute>Muts!j)}.  
+    INV \<lbrace>\<acute>Mul_mut_init n \<and> Z (\<acute>Muts!j)\<rbrace>  
   DO Mul_Redirect_Edge j n ;; 
      Mul_Color_Target j n 
   OD"
@@ -67,7 +67,7 @@
 
 lemma Mul_Color_Target: "0\<le>j \<and> j<n \<Longrightarrow> 
   \<turnstile>  Mul_Color_Target j n  
-    .{\<acute>Mul_mut_init n \<and> Z (\<acute>Muts!j)}."
+    \<lbrace>\<acute>Mul_mut_init n \<and> Z (\<acute>Muts!j)\<rbrace>"
 apply (unfold mul_mutator_defs)
 apply annhoare
 apply(simp_all)
@@ -76,7 +76,7 @@
 done
 
 lemma Mul_Mutator: "0\<le>j \<and> j<n \<Longrightarrow>  
- \<turnstile> Mul_Mutator j n .{False}."
+ \<turnstile> Mul_Mutator j n \<lbrace>False\<rbrace>"
 apply(unfold Mul_Mutator_def)
 apply annhoare
 apply(simp_all add:Mul_Redirect_Edge Mul_Color_Target)
@@ -139,13 +139,13 @@
 subsubsection {* Modular Parameterized Mutators *}
 
 lemma Mul_Parameterized_Mutators: "0<n \<Longrightarrow>
- \<parallel>- .{\<acute>Mul_mut_init n \<and> (\<forall>i<n. Z (\<acute>Muts!i))}.
+ \<parallel>- \<lbrace>\<acute>Mul_mut_init n \<and> (\<forall>i<n. Z (\<acute>Muts!i))\<rbrace>
  COBEGIN
  SCHEME  [0\<le> j< n]
   Mul_Mutator j n
- .{False}.
+ \<lbrace>False\<rbrace>
  COEND
- .{False}."
+ \<lbrace>False\<rbrace>"
 apply oghoare
 apply(force simp add:Mul_Mutator_def mul_mutator_defs nth_list_update)
 apply(erule Mul_Mutator)
@@ -175,22 +175,22 @@
 
 definition Mul_Blacken_Roots :: "nat \<Rightarrow>  mul_gar_coll_state ann_com" where
   "Mul_Blacken_Roots n \<equiv>
-  .{\<acute>Mul_Proper n}.
+  \<lbrace>\<acute>Mul_Proper n\<rbrace>
   \<acute>ind:=0;;
-  .{\<acute>Mul_Proper n \<and> \<acute>ind=0}.
+  \<lbrace>\<acute>Mul_Proper n \<and> \<acute>ind=0\<rbrace>
   WHILE \<acute>ind<length \<acute>M 
-    INV .{\<acute>Mul_Proper n \<and> (\<forall>i<\<acute>ind. i\<in>Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind\<le>length \<acute>M}.
-  DO .{\<acute>Mul_Proper n \<and> (\<forall>i<\<acute>ind. i\<in>Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M}.
+    INV \<lbrace>\<acute>Mul_Proper n \<and> (\<forall>i<\<acute>ind. i\<in>Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind\<le>length \<acute>M\<rbrace>
+  DO \<lbrace>\<acute>Mul_Proper n \<and> (\<forall>i<\<acute>ind. i\<in>Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M\<rbrace>
        IF \<acute>ind\<in>Roots THEN 
-     .{\<acute>Mul_Proper n \<and> (\<forall>i<\<acute>ind. i\<in>Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M \<and> \<acute>ind\<in>Roots}. 
+     \<lbrace>\<acute>Mul_Proper n \<and> (\<forall>i<\<acute>ind. i\<in>Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M \<and> \<acute>ind\<in>Roots\<rbrace> 
        \<acute>M:=\<acute>M[\<acute>ind:=Black] FI;;
-     .{\<acute>Mul_Proper n \<and> (\<forall>i<\<acute>ind+1. i\<in>Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M}.
+     \<lbrace>\<acute>Mul_Proper n \<and> (\<forall>i<\<acute>ind+1. i\<in>Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M\<rbrace>
        \<acute>ind:=\<acute>ind+1 
   OD"
 
 lemma Mul_Blacken_Roots: 
   "\<turnstile> Mul_Blacken_Roots n  
-  .{\<acute>Mul_Proper n \<and> Roots \<subseteq> Blacks \<acute>M}."
+  \<lbrace>\<acute>Mul_Proper n \<and> Roots \<subseteq> Blacks \<acute>M\<rbrace>"
 apply (unfold Mul_Blacken_Roots_def)
 apply annhoare
 apply(simp_all add:mul_collector_defs Graph_defs)
@@ -213,40 +213,40 @@
 
 definition Mul_Propagate_Black :: "nat \<Rightarrow>  mul_gar_coll_state ann_com" where
   "Mul_Propagate_Black n \<equiv>
- .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
-  \<and> (\<acute>Safe \<or> \<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M)}. 
+ \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
+  \<and> (\<acute>Safe \<or> \<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M)\<rbrace> 
  \<acute>ind:=0;;
- .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
+ \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
    \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> Blacks \<acute>M\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
-   \<and> (\<acute>Safe \<or> \<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M) \<and> \<acute>ind=0}. 
+   \<and> (\<acute>Safe \<or> \<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M) \<and> \<acute>ind=0\<rbrace> 
  WHILE \<acute>ind<length \<acute>E 
-  INV .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
+  INV \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
         \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
-        \<and> \<acute>Mul_PBInv \<and> \<acute>ind\<le>length \<acute>E}.
- DO .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
+        \<and> \<acute>Mul_PBInv \<and> \<acute>ind\<le>length \<acute>E\<rbrace>
+ DO \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
      \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
-     \<and> \<acute>Mul_PBInv \<and> \<acute>ind<length \<acute>E}.
+     \<and> \<acute>Mul_PBInv \<and> \<acute>ind<length \<acute>E\<rbrace>
    IF \<acute>M!(fst (\<acute>E!\<acute>ind))=Black THEN 
-   .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
+   \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
      \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
-     \<and> \<acute>Mul_PBInv \<and> (\<acute>M!fst(\<acute>E!\<acute>ind))=Black \<and> \<acute>ind<length \<acute>E}.
+     \<and> \<acute>Mul_PBInv \<and> (\<acute>M!fst(\<acute>E!\<acute>ind))=Black \<and> \<acute>ind<length \<acute>E\<rbrace>
     \<acute>k:=snd(\<acute>E!\<acute>ind);;
-   .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
+   \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
      \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
      \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>M \<or> \<acute>l<\<acute>Queue \<or> (\<forall>i<\<acute>ind. \<not>BtoW(\<acute>E!i,\<acute>M)) 
         \<and> \<acute>l\<le>\<acute>Queue \<and> \<acute>Mul_Auxk ) \<and> \<acute>k<length \<acute>M \<and> \<acute>M!fst(\<acute>E!\<acute>ind)=Black 
-     \<and> \<acute>ind<length \<acute>E}.
+     \<and> \<acute>ind<length \<acute>E\<rbrace>
    \<langle>\<acute>M:=\<acute>M[\<acute>k:=Black],,\<acute>ind:=\<acute>ind+1\<rangle>
-   ELSE .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
+   ELSE \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
          \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
-         \<and> \<acute>Mul_PBInv \<and> \<acute>ind<length \<acute>E}.
+         \<and> \<acute>Mul_PBInv \<and> \<acute>ind<length \<acute>E\<rbrace>
          \<langle>IF \<acute>M!(fst (\<acute>E!\<acute>ind))\<noteq>Black THEN \<acute>ind:=\<acute>ind+1 FI\<rangle> FI
  OD"
 
 lemma Mul_Propagate_Black: 
   "\<turnstile> Mul_Propagate_Black n  
-   .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
-     \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>M \<or> \<acute>l<\<acute>Queue \<and> (\<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))}."
+   \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
+     \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>M \<or> \<acute>l<\<acute>Queue \<and> (\<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))\<rbrace>"
 apply(unfold Mul_Propagate_Black_def)
 apply annhoare
 apply(simp_all add:Mul_PBInv_def mul_collector_defs Mul_Auxk_def Graph6 Graph7 Graph8 Graph12 mul_collector_defs Queue_def)
@@ -295,51 +295,51 @@
 
 definition Mul_Count :: "nat \<Rightarrow>  mul_gar_coll_state ann_com" where
   "Mul_Count n \<equiv> 
-  .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
+  \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
     \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
     \<and> length \<acute>Ma=length \<acute>M 
     \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M) ) 
-    \<and> \<acute>q<n+1 \<and> \<acute>bc={}}.
+    \<and> \<acute>q<n+1 \<and> \<acute>bc={}\<rbrace>
   \<acute>ind:=0;;
-  .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
+  \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
     \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
     \<and> length \<acute>Ma=length \<acute>M 
     \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M) ) 
-    \<and> \<acute>q<n+1 \<and> \<acute>bc={} \<and> \<acute>ind=0}.
+    \<and> \<acute>q<n+1 \<and> \<acute>bc={} \<and> \<acute>ind=0\<rbrace>
   WHILE \<acute>ind<length \<acute>M 
-     INV .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
+     INV \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
           \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M  
           \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>Mul_CountInv \<acute>ind 
           \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))
-          \<and> \<acute>q<n+1 \<and> \<acute>ind\<le>length \<acute>M}.
-  DO .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
+          \<and> \<acute>q<n+1 \<and> \<acute>ind\<le>length \<acute>M\<rbrace>
+  DO \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
        \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
        \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>Mul_CountInv \<acute>ind 
        \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))
-       \<and> \<acute>q<n+1 \<and> \<acute>ind<length \<acute>M}. 
+       \<and> \<acute>q<n+1 \<and> \<acute>ind<length \<acute>M\<rbrace> 
      IF \<acute>M!\<acute>ind=Black 
-     THEN .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
+     THEN \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
             \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M  
             \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>Mul_CountInv \<acute>ind 
             \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))
-            \<and> \<acute>q<n+1 \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black}.
+            \<and> \<acute>q<n+1 \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black\<rbrace>
           \<acute>bc:=insert \<acute>ind \<acute>bc
      FI;;
-  .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
+  \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
     \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
     \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>Mul_CountInv (\<acute>ind+1) 
     \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))
-    \<and> \<acute>q<n+1 \<and> \<acute>ind<length \<acute>M}.
+    \<and> \<acute>q<n+1 \<and> \<acute>ind<length \<acute>M\<rbrace>
   \<acute>ind:=\<acute>ind+1
   OD"
  
 lemma Mul_Count: 
   "\<turnstile> Mul_Count n  
-  .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
+  \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
     \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
     \<and> length \<acute>Ma=length \<acute>M \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc 
     \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M)) 
-    \<and> \<acute>q<n+1}."
+    \<and> \<acute>q<n+1\<rbrace>"
 apply (unfold Mul_Count_def)
 apply annhoare
 apply(simp_all add:Mul_CountInv_def mul_collector_defs Mul_Auxk_def Graph6 Graph7 Graph8 Graph12 mul_collector_defs Queue_def)
@@ -393,26 +393,26 @@
 
 definition Mul_Append :: "nat \<Rightarrow>  mul_gar_coll_state ann_com" where
   "Mul_Append n \<equiv> 
-  .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe}.
+  \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe\<rbrace>
   \<acute>ind:=0;;
-  .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe \<and> \<acute>ind=0}.
+  \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe \<and> \<acute>ind=0\<rbrace>
   WHILE \<acute>ind<length \<acute>M 
-    INV .{\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>M}.
-  DO .{\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M}.
+    INV \<lbrace>\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>M\<rbrace>
+  DO \<lbrace>\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M\<rbrace>
       IF \<acute>M!\<acute>ind=Black THEN 
-     .{\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black}. 
+     \<lbrace>\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black\<rbrace> 
       \<acute>M:=\<acute>M[\<acute>ind:=White] 
       ELSE 
-     .{\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>ind\<notin>Reach \<acute>E}. 
+     \<lbrace>\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>ind\<notin>Reach \<acute>E\<rbrace> 
       \<acute>E:=Append_to_free(\<acute>ind,\<acute>E)
       FI;;
-  .{\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv (\<acute>ind+1) \<and> \<acute>ind<length \<acute>M}. 
+  \<lbrace>\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv (\<acute>ind+1) \<and> \<acute>ind<length \<acute>M\<rbrace> 
    \<acute>ind:=\<acute>ind+1
   OD"
 
 lemma Mul_Append: 
   "\<turnstile> Mul_Append n  
-     .{\<acute>Mul_Proper n}."
+     \<lbrace>\<acute>Mul_Proper n\<rbrace>"
 apply(unfold Mul_Append_def)
 apply annhoare
 apply(simp_all add: mul_collector_defs Mul_AppendInv_def 
@@ -431,52 +431,52 @@
 
 definition Mul_Collector :: "nat \<Rightarrow>  mul_gar_coll_state ann_com" where
   "Mul_Collector n \<equiv>
-.{\<acute>Mul_Proper n}.  
-WHILE True INV .{\<acute>Mul_Proper n}. 
+\<lbrace>\<acute>Mul_Proper n\<rbrace>  
+WHILE True INV \<lbrace>\<acute>Mul_Proper n\<rbrace> 
 DO  
 Mul_Blacken_Roots n ;; 
-.{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M}.  
+\<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M\<rbrace>  
  \<acute>obc:={};; 
-.{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={}}.  
+\<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={}\<rbrace>  
  \<acute>bc:=Roots;; 
-.{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots}. 
+\<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots\<rbrace> 
  \<acute>l:=0;; 
-.{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots \<and> \<acute>l=0}. 
+\<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots \<and> \<acute>l=0\<rbrace> 
  WHILE \<acute>l<n+1  
-   INV .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and>  
-         (\<acute>Safe \<or> (\<acute>l\<le>\<acute>Queue \<or> \<acute>bc\<subset>Blacks \<acute>M) \<and> \<acute>l<n+1)}. 
- DO .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
-      \<and> (\<acute>Safe \<or> \<acute>l\<le>\<acute>Queue \<or> \<acute>bc\<subset>Blacks \<acute>M)}.
+   INV \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and>  
+         (\<acute>Safe \<or> (\<acute>l\<le>\<acute>Queue \<or> \<acute>bc\<subset>Blacks \<acute>M) \<and> \<acute>l<n+1)\<rbrace> 
+ DO \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
+      \<and> (\<acute>Safe \<or> \<acute>l\<le>\<acute>Queue \<or> \<acute>bc\<subset>Blacks \<acute>M)\<rbrace>
     \<acute>obc:=\<acute>bc;;
     Mul_Propagate_Black n;; 
-    .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
+    \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
       \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
       \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>M \<or> \<acute>l<\<acute>Queue 
-      \<and> (\<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))}. 
+      \<and> (\<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))\<rbrace> 
     \<acute>bc:={};;
-    .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
+    \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
       \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
       \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>M \<or> \<acute>l<\<acute>Queue 
-      \<and> (\<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M)) \<and> \<acute>bc={}}. 
+      \<and> (\<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M)) \<and> \<acute>bc={}\<rbrace> 
        \<langle> \<acute>Ma:=\<acute>M,, \<acute>q:=\<acute>Queue \<rangle>;;
     Mul_Count n;; 
-    .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
+    \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
       \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
       \<and> length \<acute>Ma=length \<acute>M \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc 
       \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M)) 
-      \<and> \<acute>q<n+1}. 
+      \<and> \<acute>q<n+1\<rbrace> 
     IF \<acute>obc=\<acute>bc THEN
-    .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
+    \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
       \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
       \<and> length \<acute>Ma=length \<acute>M \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc 
       \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M)) 
-      \<and> \<acute>q<n+1 \<and> \<acute>obc=\<acute>bc}.  
+      \<and> \<acute>q<n+1 \<and> \<acute>obc=\<acute>bc\<rbrace>  
     \<acute>l:=\<acute>l+1  
-    ELSE .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
+    ELSE \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
           \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
           \<and> length \<acute>Ma=length \<acute>M \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc 
           \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M)) 
-          \<and> \<acute>q<n+1 \<and> \<acute>obc\<noteq>\<acute>bc}.  
+          \<and> \<acute>q<n+1 \<and> \<acute>obc\<noteq>\<acute>bc\<rbrace>  
         \<acute>l:=0 FI 
  OD;; 
  Mul_Append n  
@@ -488,7 +488,7 @@
 
 lemma Mul_Collector:
   "\<turnstile> Mul_Collector n 
-  .{False}."
+  \<lbrace>False\<rbrace>"
 apply(unfold Mul_Collector_def)
 apply annhoare
 apply(simp_all only:pre.simps Mul_Blacken_Roots 
@@ -1237,16 +1237,16 @@
 text {* The total number of verification conditions is 328 *}
 
 lemma Mul_Gar_Coll: 
- "\<parallel>- .{\<acute>Mul_Proper n \<and> \<acute>Mul_mut_init n \<and> (\<forall>i<n. Z (\<acute>Muts!i))}.  
+ "\<parallel>- \<lbrace>\<acute>Mul_Proper n \<and> \<acute>Mul_mut_init n \<and> (\<forall>i<n. Z (\<acute>Muts!i))\<rbrace>  
  COBEGIN  
   Mul_Collector n
- .{False}.
+ \<lbrace>False\<rbrace>
  \<parallel>  
  SCHEME  [0\<le> j< n]
   Mul_Mutator j n
- .{False}.  
+ \<lbrace>False\<rbrace>  
  COEND  
- .{False}."
+ \<lbrace>False\<rbrace>"
 apply oghoare
 --{* Strengthening the precondition *}
 apply(rule Int_greatest)
diff -r 07593a0a27f4 -r effd8fcabca2 src/HOL/Hoare_Parallel/OG_Examples.thy
--- a/src/HOL/Hoare_Parallel/OG_Examples.thy	Tue Aug 27 23:54:23 2013 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Examples.thy	Wed Aug 28 00:18:50 2013 +0200
@@ -16,30 +16,30 @@
  hold :: nat
 
 lemma Petersons_mutex_1: 
-  "\<parallel>- .{\<acute>pr1=0 \<and> \<not>\<acute>in1 \<and> \<acute>pr2=0 \<and> \<not>\<acute>in2 }.  
-  COBEGIN .{\<acute>pr1=0 \<and> \<not>\<acute>in1}.  
-  WHILE True INV .{\<acute>pr1=0 \<and> \<not>\<acute>in1}.  
+  "\<parallel>- \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1 \<and> \<acute>pr2=0 \<and> \<not>\<acute>in2 \<rbrace>  
+  COBEGIN \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1\<rbrace>  
+  WHILE True INV \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1\<rbrace>  
   DO  
-  .{\<acute>pr1=0 \<and> \<not>\<acute>in1}. \<langle> \<acute>in1:=True,,\<acute>pr1:=1 \<rangle>;;  
-  .{\<acute>pr1=1 \<and> \<acute>in1}.  \<langle> \<acute>hold:=1,,\<acute>pr1:=2 \<rangle>;;  
-  .{\<acute>pr1=2 \<and> \<acute>in1 \<and> (\<acute>hold=1 \<or> \<acute>hold=2 \<and> \<acute>pr2=2)}.  
+  \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1\<rbrace> \<langle> \<acute>in1:=True,,\<acute>pr1:=1 \<rangle>;;  
+  \<lbrace>\<acute>pr1=1 \<and> \<acute>in1\<rbrace>  \<langle> \<acute>hold:=1,,\<acute>pr1:=2 \<rangle>;;  
+  \<lbrace>\<acute>pr1=2 \<and> \<acute>in1 \<and> (\<acute>hold=1 \<or> \<acute>hold=2 \<and> \<acute>pr2=2)\<rbrace>  
   AWAIT (\<not>\<acute>in2 \<or> \<not>(\<acute>hold=1)) THEN \<acute>pr1:=3 END;;    
-  .{\<acute>pr1=3 \<and> \<acute>in1 \<and> (\<acute>hold=1 \<or> \<acute>hold=2 \<and> \<acute>pr2=2)}. 
+  \<lbrace>\<acute>pr1=3 \<and> \<acute>in1 \<and> (\<acute>hold=1 \<or> \<acute>hold=2 \<and> \<acute>pr2=2)\<rbrace> 
    \<langle>\<acute>in1:=False,,\<acute>pr1:=0\<rangle> 
-  OD .{\<acute>pr1=0 \<and> \<not>\<acute>in1}.  
+  OD \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1\<rbrace>  
   \<parallel>  
-  .{\<acute>pr2=0 \<and> \<not>\<acute>in2}.  
-  WHILE True INV .{\<acute>pr2=0 \<and> \<not>\<acute>in2}.  
+  \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace>  
+  WHILE True INV \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace>  
   DO  
-  .{\<acute>pr2=0 \<and> \<not>\<acute>in2}. \<langle> \<acute>in2:=True,,\<acute>pr2:=1 \<rangle>;;  
-  .{\<acute>pr2=1 \<and> \<acute>in2}. \<langle>  \<acute>hold:=2,,\<acute>pr2:=2 \<rangle>;;  
-  .{\<acute>pr2=2 \<and> \<acute>in2 \<and> (\<acute>hold=2 \<or> (\<acute>hold=1 \<and> \<acute>pr1=2))}.  
+  \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace> \<langle> \<acute>in2:=True,,\<acute>pr2:=1 \<rangle>;;  
+  \<lbrace>\<acute>pr2=1 \<and> \<acute>in2\<rbrace> \<langle>  \<acute>hold:=2,,\<acute>pr2:=2 \<rangle>;;  
+  \<lbrace>\<acute>pr2=2 \<and> \<acute>in2 \<and> (\<acute>hold=2 \<or> (\<acute>hold=1 \<and> \<acute>pr1=2))\<rbrace>  
   AWAIT (\<not>\<acute>in1 \<or> \<not>(\<acute>hold=2)) THEN \<acute>pr2:=3  END;;    
-  .{\<acute>pr2=3 \<and> \<acute>in2 \<and> (\<acute>hold=2 \<or> (\<acute>hold=1 \<and> \<acute>pr1=2))}. 
+  \<lbrace>\<acute>pr2=3 \<and> \<acute>in2 \<and> (\<acute>hold=2 \<or> (\<acute>hold=1 \<and> \<acute>pr1=2))\<rbrace> 
     \<langle>\<acute>in2:=False,,\<acute>pr2:=0\<rangle> 
-  OD .{\<acute>pr2=0 \<and> \<not>\<acute>in2}.  
+  OD \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace>  
   COEND  
-  .{\<acute>pr1=0 \<and> \<not>\<acute>in1 \<and> \<acute>pr2=0 \<and> \<not>\<acute>in2}."
+  \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1 \<and> \<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace>"
 apply oghoare
 --{* 104 verification conditions. *}
 apply auto
@@ -57,37 +57,37 @@
  after2 :: bool
 
 lemma Busy_wait_mutex: 
- "\<parallel>-  .{True}.  
+ "\<parallel>-  \<lbrace>True\<rbrace>  
   \<acute>flag1:=False,, \<acute>flag2:=False,,  
-  COBEGIN .{\<not>\<acute>flag1}.  
+  COBEGIN \<lbrace>\<not>\<acute>flag1\<rbrace>  
         WHILE True  
-        INV .{\<not>\<acute>flag1}.  
-        DO .{\<not>\<acute>flag1}. \<langle> \<acute>flag1:=True,,\<acute>after1:=False \<rangle>;;  
-           .{\<acute>flag1 \<and> \<not>\<acute>after1}. \<langle> \<acute>turn:=1,,\<acute>after1:=True \<rangle>;;  
-           .{\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)}.  
+        INV \<lbrace>\<not>\<acute>flag1\<rbrace>  
+        DO \<lbrace>\<not>\<acute>flag1\<rbrace> \<langle> \<acute>flag1:=True,,\<acute>after1:=False \<rangle>;;  
+           \<lbrace>\<acute>flag1 \<and> \<not>\<acute>after1\<rbrace> \<langle> \<acute>turn:=1,,\<acute>after1:=True \<rangle>;;  
+           \<lbrace>\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)\<rbrace>  
             WHILE \<not>(\<acute>flag2 \<longrightarrow> \<acute>turn=2)  
-            INV .{\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)}.  
-            DO .{\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)}. SKIP OD;; 
-           .{\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>flag2 \<and> \<acute>after2 \<longrightarrow> \<acute>turn=2)}.
+            INV \<lbrace>\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)\<rbrace>  
+            DO \<lbrace>\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)\<rbrace> SKIP OD;; 
+           \<lbrace>\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>flag2 \<and> \<acute>after2 \<longrightarrow> \<acute>turn=2)\<rbrace>
             \<acute>flag1:=False  
         OD  
-       .{False}.  
+       \<lbrace>False\<rbrace>  
   \<parallel>  
-     .{\<not>\<acute>flag2}.  
+     \<lbrace>\<not>\<acute>flag2\<rbrace>  
         WHILE True  
-        INV .{\<not>\<acute>flag2}.  
-        DO .{\<not>\<acute>flag2}. \<langle> \<acute>flag2:=True,,\<acute>after2:=False \<rangle>;;  
-           .{\<acute>flag2 \<and> \<not>\<acute>after2}. \<langle> \<acute>turn:=2,,\<acute>after2:=True \<rangle>;;  
-           .{\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)}.  
+        INV \<lbrace>\<not>\<acute>flag2\<rbrace>  
+        DO \<lbrace>\<not>\<acute>flag2\<rbrace> \<langle> \<acute>flag2:=True,,\<acute>after2:=False \<rangle>;;  
+           \<lbrace>\<acute>flag2 \<and> \<not>\<acute>after2\<rbrace> \<langle> \<acute>turn:=2,,\<acute>after2:=True \<rangle>;;  
+           \<lbrace>\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)\<rbrace>  
             WHILE \<not>(\<acute>flag1 \<longrightarrow> \<acute>turn=1)  
-            INV .{\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)}.  
-            DO .{\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)}. SKIP OD;;  
-           .{\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>flag1 \<and> \<acute>after1 \<longrightarrow> \<acute>turn=1)}. 
+            INV \<lbrace>\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)\<rbrace>  
+            DO \<lbrace>\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)\<rbrace> SKIP OD;;  
+           \<lbrace>\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>flag1 \<and> \<acute>after1 \<longrightarrow> \<acute>turn=1)\<rbrace> 
             \<acute>flag2:=False  
         OD  
-       .{False}.  
+       \<lbrace>False\<rbrace>  
   COEND  
-  .{False}."
+  \<lbrace>False\<rbrace>"
 apply oghoare
 --{* 122 vc *}
 apply auto
@@ -100,21 +100,21 @@
  who :: nat
 
 lemma Semaphores_mutex: 
- "\<parallel>- .{i\<noteq>j}.  
+ "\<parallel>- \<lbrace>i\<noteq>j\<rbrace>  
   \<acute>out:=True ,,  
-  COBEGIN .{i\<noteq>j}.  
-       WHILE True INV .{i\<noteq>j}.  
-       DO .{i\<noteq>j}. AWAIT \<acute>out THEN  \<acute>out:=False,, \<acute>who:=i END;;  
-          .{\<not>\<acute>out \<and> \<acute>who=i \<and> i\<noteq>j}. \<acute>out:=True OD  
-       .{False}.  
+  COBEGIN \<lbrace>i\<noteq>j\<rbrace>  
+       WHILE True INV \<lbrace>i\<noteq>j\<rbrace>  
+       DO \<lbrace>i\<noteq>j\<rbrace> AWAIT \<acute>out THEN  \<acute>out:=False,, \<acute>who:=i END;;  
+          \<lbrace>\<not>\<acute>out \<and> \<acute>who=i \<and> i\<noteq>j\<rbrace> \<acute>out:=True OD  
+       \<lbrace>False\<rbrace>  
   \<parallel>  
-       .{i\<noteq>j}.  
-       WHILE True INV .{i\<noteq>j}.  
-       DO .{i\<noteq>j}. AWAIT \<acute>out THEN  \<acute>out:=False,,\<acute>who:=j END;;  
-          .{\<not>\<acute>out \<and> \<acute>who=j \<and> i\<noteq>j}. \<acute>out:=True OD  
-       .{False}.  
+       \<lbrace>i\<noteq>j\<rbrace>  
+       WHILE True INV \<lbrace>i\<noteq>j\<rbrace>  
+       DO \<lbrace>i\<noteq>j\<rbrace> AWAIT \<acute>out THEN  \<acute>out:=False,,\<acute>who:=j END;;  
+          \<lbrace>\<not>\<acute>out \<and> \<acute>who=j \<and> i\<noteq>j\<rbrace> \<acute>out:=True OD  
+       \<lbrace>False\<rbrace>  
   COEND  
-  .{False}."
+  \<lbrace>False\<rbrace>"
 apply oghoare
 --{* 38 vc *}
 apply auto
@@ -123,17 +123,17 @@
 subsubsection {* Peterson's Algorithm III: Parameterized version: *}
 
 lemma Semaphores_parameterized_mutex: 
- "0<n \<Longrightarrow> \<parallel>- .{True}.  
+ "0<n \<Longrightarrow> \<parallel>- \<lbrace>True\<rbrace>  
   \<acute>out:=True ,,  
  COBEGIN
   SCHEME [0\<le> i< n]
-    .{True}.  
-     WHILE True INV .{True}.  
-      DO .{True}. AWAIT \<acute>out THEN  \<acute>out:=False,, \<acute>who:=i END;;  
-         .{\<not>\<acute>out \<and> \<acute>who=i}. \<acute>out:=True OD
-    .{False}. 
+    \<lbrace>True\<rbrace>  
+     WHILE True INV \<lbrace>True\<rbrace>  
+      DO \<lbrace>True\<rbrace> AWAIT \<acute>out THEN  \<acute>out:=False,, \<acute>who:=i END;;  
+         \<lbrace>\<not>\<acute>out \<and> \<acute>who=i\<rbrace> \<acute>out:=True OD
+    \<lbrace>False\<rbrace> 
  COEND
-  .{False}." 
+  \<lbrace>False\<rbrace>" 
 apply oghoare
 --{* 20 vc *}
 apply auto
@@ -150,22 +150,22 @@
 lemma Ticket_mutex: 
  "\<lbrakk> 0<n; I=\<guillemotleft>n=length \<acute>turn \<and> 0<\<acute>nextv \<and> (\<forall>k l. k<n \<and> l<n \<and> k\<noteq>l 
     \<longrightarrow> \<acute>turn!k < \<acute>num \<and> (\<acute>turn!k =0 \<or> \<acute>turn!k\<noteq>\<acute>turn!l))\<guillemotright> \<rbrakk>
-   \<Longrightarrow> \<parallel>- .{n=length \<acute>turn}.  
+   \<Longrightarrow> \<parallel>- \<lbrace>n=length \<acute>turn\<rbrace>  
    \<acute>index:= 0,,
-   WHILE \<acute>index < n INV .{n=length \<acute>turn \<and> (\<forall>i<\<acute>index. \<acute>turn!i=0)}. 
+   WHILE \<acute>index < n INV \<lbrace>n=length \<acute>turn \<and> (\<forall>i<\<acute>index. \<acute>turn!i=0)\<rbrace> 
     DO \<acute>turn:= \<acute>turn[\<acute>index:=0],, \<acute>index:=\<acute>index +1 OD,,
   \<acute>num:=1 ,, \<acute>nextv:=1 ,, 
  COBEGIN
   SCHEME [0\<le> i< n]
-    .{\<acute>I}.  
-     WHILE True INV .{\<acute>I}.  
-      DO .{\<acute>I}. \<langle> \<acute>turn :=\<acute>turn[i:=\<acute>num],, \<acute>num:=\<acute>num+1 \<rangle>;;  
-         .{\<acute>I}. WAIT \<acute>turn!i=\<acute>nextv END;;
-         .{\<acute>I \<and> \<acute>turn!i=\<acute>nextv}. \<acute>nextv:=\<acute>nextv+1
+    \<lbrace>\<acute>I\<rbrace>  
+     WHILE True INV \<lbrace>\<acute>I\<rbrace>  
+      DO \<lbrace>\<acute>I\<rbrace> \<langle> \<acute>turn :=\<acute>turn[i:=\<acute>num],, \<acute>num:=\<acute>num+1 \<rangle>;;  
+         \<lbrace>\<acute>I\<rbrace> WAIT \<acute>turn!i=\<acute>nextv END;;
+         \<lbrace>\<acute>I \<and> \<acute>turn!i=\<acute>nextv\<rbrace> \<acute>nextv:=\<acute>nextv+1
       OD
-    .{False}. 
+    \<lbrace>False\<rbrace> 
  COEND
-  .{False}." 
+  \<lbrace>False\<rbrace>" 
 apply oghoare
 --{* 35 vc *}
 apply simp_all
@@ -259,40 +259,40 @@
       \<and> (\<not>\<acute>found \<and> a<\<acute> x \<longrightarrow> f(\<acute>x)\<noteq>0) \<guillemotright> ;  
     I2= \<guillemotleft>\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> (a<\<acute>x \<and> f(\<acute>x)=0) \<or> (\<acute>y\<le>a \<and> f(\<acute>y)=0)) 
       \<and> (\<not>\<acute>found \<and> \<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0) \<guillemotright> \<rbrakk> \<Longrightarrow>  
-  \<parallel>- .{\<exists> u. f(u)=0}.  
+  \<parallel>- \<lbrace>\<exists> u. f(u)=0\<rbrace>  
   \<acute>turn:=1,, \<acute>found:= False,,  
   \<acute>x:=a,, \<acute>y:=a+1 ,,  
-  COBEGIN .{\<acute>I1}.  
+  COBEGIN \<lbrace>\<acute>I1\<rbrace>  
        WHILE \<not>\<acute>found  
-       INV .{\<acute>I1}.  
-       DO .{a\<le>\<acute>x \<and> (\<acute>found \<longrightarrow> \<acute>y\<le>a \<and> f(\<acute>y)=0) \<and> (a<\<acute>x \<longrightarrow> f(\<acute>x)\<noteq>0)}.  
+       INV \<lbrace>\<acute>I1\<rbrace>  
+       DO \<lbrace>a\<le>\<acute>x \<and> (\<acute>found \<longrightarrow> \<acute>y\<le>a \<and> f(\<acute>y)=0) \<and> (a<\<acute>x \<longrightarrow> f(\<acute>x)\<noteq>0)\<rbrace>  
           WAIT \<acute>turn=1 END;;  
-          .{a\<le>\<acute>x \<and> (\<acute>found \<longrightarrow> \<acute>y\<le>a \<and> f(\<acute>y)=0) \<and> (a<\<acute>x \<longrightarrow> f(\<acute>x)\<noteq>0)}.  
+          \<lbrace>a\<le>\<acute>x \<and> (\<acute>found \<longrightarrow> \<acute>y\<le>a \<and> f(\<acute>y)=0) \<and> (a<\<acute>x \<longrightarrow> f(\<acute>x)\<noteq>0)\<rbrace>  
           \<acute>turn:=2;;  
-          .{a\<le>\<acute>x \<and> (\<acute>found \<longrightarrow> \<acute>y\<le>a \<and> f(\<acute>y)=0) \<and> (a<\<acute>x \<longrightarrow> f(\<acute>x)\<noteq>0)}.    
+          \<lbrace>a\<le>\<acute>x \<and> (\<acute>found \<longrightarrow> \<acute>y\<le>a \<and> f(\<acute>y)=0) \<and> (a<\<acute>x \<longrightarrow> f(\<acute>x)\<noteq>0)\<rbrace>    
           \<langle> \<acute>x:=\<acute>x+1,,  
             IF f(\<acute>x)=0 THEN \<acute>found:=True ELSE SKIP FI\<rangle>  
        OD;;  
-       .{\<acute>I1  \<and> \<acute>found}.  
+       \<lbrace>\<acute>I1  \<and> \<acute>found\<rbrace>  
        \<acute>turn:=2  
-       .{\<acute>I1 \<and> \<acute>found}.  
+       \<lbrace>\<acute>I1 \<and> \<acute>found\<rbrace>  
   \<parallel>  
-      .{\<acute>I2}.  
+      \<lbrace>\<acute>I2\<rbrace>  
        WHILE \<not>\<acute>found  
-       INV .{\<acute>I2}.  
-       DO .{\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> a<\<acute>x \<and> f(\<acute>x)=0) \<and> (\<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0)}.  
+       INV \<lbrace>\<acute>I2\<rbrace>  
+       DO \<lbrace>\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> a<\<acute>x \<and> f(\<acute>x)=0) \<and> (\<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0)\<rbrace>  
           WAIT \<acute>turn=2 END;;  
-          .{\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> a<\<acute>x \<and> f(\<acute>x)=0) \<and> (\<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0)}.  
+          \<lbrace>\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> a<\<acute>x \<and> f(\<acute>x)=0) \<and> (\<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0)\<rbrace>  
           \<acute>turn:=1;;  
-          .{\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> a<\<acute>x \<and> f(\<acute>x)=0) \<and> (\<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0)}.  
+          \<lbrace>\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> a<\<acute>x \<and> f(\<acute>x)=0) \<and> (\<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0)\<rbrace>  
           \<langle> \<acute>y:=(\<acute>y - 1),,  
             IF f(\<acute>y)=0 THEN \<acute>found:=True ELSE SKIP FI\<rangle>  
        OD;;  
-       .{\<acute>I2 \<and> \<acute>found}.  
+       \<lbrace>\<acute>I2 \<and> \<acute>found\<rbrace>  
        \<acute>turn:=1  
-       .{\<acute>I2 \<and> \<acute>found}.  
+       \<lbrace>\<acute>I2 \<and> \<acute>found\<rbrace>  
   COEND  
-  .{f(\<acute>x)=0 \<or> f(\<acute>y)=0}."
+  \<lbrace>f(\<acute>x)=0 \<or> f(\<acute>y)=0\<rbrace>"
 apply oghoare
 --{* 98 verification conditions *}
 apply auto 
@@ -306,26 +306,26 @@
     \<and> (\<not>\<acute>found \<and> a<\<acute>x \<longrightarrow> f(\<acute>x)\<noteq>0)\<guillemotright>;  
  I2= \<guillemotleft>\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> (a<\<acute>x \<and> f(\<acute>x)=0) \<or> (\<acute>y\<le>a \<and> f(\<acute>y)=0)) 
     \<and> (\<not>\<acute>found \<and> \<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0)\<guillemotright>\<rbrakk> \<Longrightarrow>  
-  \<parallel>- .{\<exists>u. f(u)=0}.  
+  \<parallel>- \<lbrace>\<exists>u. f(u)=0\<rbrace>  
   \<acute>found:= False,,  
   \<acute>x:=a,, \<acute>y:=a+1,,  
-  COBEGIN .{\<acute>I1}.  
+  COBEGIN \<lbrace>\<acute>I1\<rbrace>  
        WHILE \<not>\<acute>found  
-       INV .{\<acute>I1}.  
-       DO .{a\<le>\<acute>x \<and> (\<acute>found \<longrightarrow> \<acute>y\<le>a \<and> f(\<acute>y)=0) \<and> (a<\<acute>x \<longrightarrow> f(\<acute>x)\<noteq>0)}.  
+       INV \<lbrace>\<acute>I1\<rbrace>  
+       DO \<lbrace>a\<le>\<acute>x \<and> (\<acute>found \<longrightarrow> \<acute>y\<le>a \<and> f(\<acute>y)=0) \<and> (a<\<acute>x \<longrightarrow> f(\<acute>x)\<noteq>0)\<rbrace>  
           \<langle> \<acute>x:=\<acute>x+1,,IF f(\<acute>x)=0 THEN  \<acute>found:=True ELSE  SKIP FI\<rangle>  
        OD  
-       .{\<acute>I1 \<and> \<acute>found}.  
+       \<lbrace>\<acute>I1 \<and> \<acute>found\<rbrace>  
   \<parallel>  
-      .{\<acute>I2}.  
+      \<lbrace>\<acute>I2\<rbrace>  
        WHILE \<not>\<acute>found  
-       INV .{\<acute>I2}.  
-       DO .{\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> a<\<acute>x \<and> f(\<acute>x)=0) \<and> (\<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0)}.  
+       INV \<lbrace>\<acute>I2\<rbrace>  
+       DO \<lbrace>\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> a<\<acute>x \<and> f(\<acute>x)=0) \<and> (\<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0)\<rbrace>  
           \<langle> \<acute>y:=(\<acute>y - 1),,IF f(\<acute>y)=0 THEN  \<acute>found:=True ELSE  SKIP FI\<rangle>  
        OD  
-       .{\<acute>I2 \<and> \<acute>found}.  
+       \<lbrace>\<acute>I2 \<and> \<acute>found\<rbrace>  
   COEND  
-  .{f(\<acute>x)=0 \<or> f(\<acute>y)=0}."
+  \<lbrace>f(\<acute>x)=0 \<or> f(\<acute>y)=0\<rbrace>"
 apply oghoare
 --{* 20 vc *}
 apply auto
@@ -390,44 +390,44 @@
     p1= \<guillemotleft>\<acute>I1 \<and> \<acute>li=\<acute>ins\<guillemotright> ;  
     I2 = \<guillemotleft>\<acute>I \<and> (\<forall>k<\<acute>lj. (a ! k)=(\<acute>b ! k)) \<and> \<acute>lj\<le>length a\<guillemotright> ;
     p2 = \<guillemotleft>\<acute>I2 \<and> \<acute>lj=\<acute>outs\<guillemotright> \<rbrakk> \<Longrightarrow>   
-  \<parallel>- .{\<acute>INIT}.  
+  \<parallel>- \<lbrace>\<acute>INIT\<rbrace>  
  \<acute>ins:=0,, \<acute>outs:=0,, \<acute>li:=0,, \<acute>lj:=0,,
- COBEGIN .{\<acute>p1 \<and> \<acute>INIT}. 
+ COBEGIN \<lbrace>\<acute>p1 \<and> \<acute>INIT\<rbrace> 
    WHILE \<acute>li <length a 
-     INV .{\<acute>p1 \<and> \<acute>INIT}.   
-   DO .{\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a}.  
+     INV \<lbrace>\<acute>p1 \<and> \<acute>INIT\<rbrace>   
+   DO \<lbrace>\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a\<rbrace>  
        \<acute>vx:= (a ! \<acute>li);;  
-      .{\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a \<and> \<acute>vx=(a ! \<acute>li)}. 
+      \<lbrace>\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a \<and> \<acute>vx=(a ! \<acute>li)\<rbrace> 
         WAIT \<acute>ins-\<acute>outs < length \<acute>buffer END;; 
-      .{\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a \<and> \<acute>vx=(a ! \<acute>li) 
-         \<and> \<acute>ins-\<acute>outs < length \<acute>buffer}. 
+      \<lbrace>\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a \<and> \<acute>vx=(a ! \<acute>li) 
+         \<and> \<acute>ins-\<acute>outs < length \<acute>buffer\<rbrace> 
        \<acute>buffer:=(list_update \<acute>buffer (\<acute>ins mod (length \<acute>buffer)) \<acute>vx);; 
-      .{\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a 
+      \<lbrace>\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a 
          \<and> (a ! \<acute>li)=(\<acute>buffer ! (\<acute>ins mod (length \<acute>buffer))) 
-         \<and> \<acute>ins-\<acute>outs <length \<acute>buffer}.  
+         \<and> \<acute>ins-\<acute>outs <length \<acute>buffer\<rbrace>  
        \<acute>ins:=\<acute>ins+1;; 
-      .{\<acute>I1 \<and> \<acute>INIT \<and> (\<acute>li+1)=\<acute>ins \<and> \<acute>li<length a}.  
+      \<lbrace>\<acute>I1 \<and> \<acute>INIT \<and> (\<acute>li+1)=\<acute>ins \<and> \<acute>li<length a\<rbrace>  
        \<acute>li:=\<acute>li+1  
    OD  
-  .{\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li=length a}.  
+  \<lbrace>\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li=length a\<rbrace>  
   \<parallel>  
-  .{\<acute>p2 \<and> \<acute>INIT}.  
+  \<lbrace>\<acute>p2 \<and> \<acute>INIT\<rbrace>  
    WHILE \<acute>lj < length a  
-     INV .{\<acute>p2 \<and> \<acute>INIT}.  
-   DO .{\<acute>p2 \<and> \<acute>lj<length a \<and> \<acute>INIT}.  
+     INV \<lbrace>\<acute>p2 \<and> \<acute>INIT\<rbrace>  
+   DO \<lbrace>\<acute>p2 \<and> \<acute>lj<length a \<and> \<acute>INIT\<rbrace>  
         WAIT \<acute>outs<\<acute>ins END;; 
-      .{\<acute>p2 \<and> \<acute>lj<length a \<and> \<acute>outs<\<acute>ins \<and> \<acute>INIT}.  
+      \<lbrace>\<acute>p2 \<and> \<acute>lj<length a \<and> \<acute>outs<\<acute>ins \<and> \<acute>INIT\<rbrace>  
        \<acute>vy:=(\<acute>buffer ! (\<acute>outs mod (length \<acute>buffer)));; 
-      .{\<acute>p2 \<and> \<acute>lj<length a \<and> \<acute>outs<\<acute>ins \<and> \<acute>vy=(a ! \<acute>lj) \<and> \<acute>INIT}.  
+      \<lbrace>\<acute>p2 \<and> \<acute>lj<length a \<and> \<acute>outs<\<acute>ins \<and> \<acute>vy=(a ! \<acute>lj) \<and> \<acute>INIT\<rbrace>  
        \<acute>outs:=\<acute>outs+1;;  
-      .{\<acute>I2 \<and> (\<acute>lj+1)=\<acute>outs \<and> \<acute>lj<length a \<and> \<acute>vy=(a ! \<acute>lj) \<and> \<acute>INIT}.  
+      \<lbrace>\<acute>I2 \<and> (\<acute>lj+1)=\<acute>outs \<and> \<acute>lj<length a \<and> \<acute>vy=(a ! \<acute>lj) \<and> \<acute>INIT\<rbrace>  
        \<acute>b:=(list_update \<acute>b \<acute>lj \<acute>vy);; 
-      .{\<acute>I2 \<and> (\<acute>lj+1)=\<acute>outs \<and> \<acute>lj<length a \<and> (a ! \<acute>lj)=(\<acute>b ! \<acute>lj) \<and> \<acute>INIT}.  
+      \<lbrace>\<acute>I2 \<and> (\<acute>lj+1)=\<acute>outs \<and> \<acute>lj<length a \<and> (a ! \<acute>lj)=(\<acute>b ! \<acute>lj) \<and> \<acute>INIT\<rbrace>  
        \<acute>lj:=\<acute>lj+1  
    OD  
-  .{\<acute>p2 \<and> \<acute>lj=length a \<and> \<acute>INIT}.  
+  \<lbrace>\<acute>p2 \<and> \<acute>lj=length a \<and> \<acute>INIT\<rbrace>  
  COEND  
- .{ \<forall>k<length a. (a ! k)=(\<acute>b ! k)}."
+ \<lbrace> \<forall>k<length a. (a ! k)=(\<acute>b ! k)\<rbrace>"
 apply oghoare
 --{* 138 vc  *}
 apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
@@ -455,9 +455,9 @@
   a :: "nat \<Rightarrow> nat"
 
 lemma Example1: 
- "\<parallel>- .{True}.
-   COBEGIN SCHEME [0\<le>i<n] .{True}. \<acute>a:=\<acute>a (i:=0) .{\<acute>a i=0}. COEND 
-  .{\<forall>i < n. \<acute>a i = 0}."
+ "\<parallel>- \<lbrace>True\<rbrace>
+   COBEGIN SCHEME [0\<le>i<n] \<lbrace>True\<rbrace> \<acute>a:=\<acute>a (i:=0) \<lbrace>\<acute>a i=0\<rbrace> COEND 
+  \<lbrace>\<forall>i < n. \<acute>a i = 0\<rbrace>"
 apply oghoare
 apply simp_all
 done
@@ -466,11 +466,11 @@
 record Example1_list =
   A :: "nat list"
 lemma Example1_list: 
- "\<parallel>- .{n < length \<acute>A}. 
+ "\<parallel>- \<lbrace>n < length \<acute>A\<rbrace> 
    COBEGIN 
-     SCHEME [0\<le>i<n] .{n < length \<acute>A}. \<acute>A:=\<acute>A[i:=0] .{\<acute>A!i=0}. 
+     SCHEME [0\<le>i<n] \<lbrace>n < length \<acute>A\<rbrace> \<acute>A:=\<acute>A[i:=0] \<lbrace>\<acute>A!i=0\<rbrace> 
    COEND 
-    .{\<forall>i < n. \<acute>A!i = 0}."
+    \<lbrace>\<forall>i < n. \<acute>A!i = 0\<rbrace>"
 apply oghoare
 apply force+
 done
@@ -525,14 +525,14 @@
  x :: nat
 
 lemma Example_2: "0<n \<Longrightarrow> 
- \<parallel>- .{\<acute>x=0 \<and> (\<Sum>i=0..<n. \<acute>c i)=0}.  
+ \<parallel>- \<lbrace>\<acute>x=0 \<and> (\<Sum>i=0..<n. \<acute>c i)=0\<rbrace>  
  COBEGIN 
    SCHEME [0\<le>i<n] 
-  .{\<acute>x=(\<Sum>i=0..<n. \<acute>c i) \<and> \<acute>c i=0}. 
+  \<lbrace>\<acute>x=(\<Sum>i=0..<n. \<acute>c i) \<and> \<acute>c i=0\<rbrace> 
    \<langle> \<acute>x:=\<acute>x+(Suc 0),, \<acute>c:=\<acute>c (i:=(Suc 0)) \<rangle>
-  .{\<acute>x=(\<Sum>i=0..<n. \<acute>c i) \<and> \<acute>c i=(Suc 0)}.
+  \<lbrace>\<acute>x=(\<Sum>i=0..<n. \<acute>c i) \<and> \<acute>c i=(Suc 0)\<rbrace>
  COEND 
- .{\<acute>x=n}."
+ \<lbrace>\<acute>x=n\<rbrace>"
 apply oghoare
 apply (simp_all cong del: strong_setsum_cong)
 apply (tactic {* ALLGOALS (clarify_tac @{context}) *})
diff -r 07593a0a27f4 -r effd8fcabca2 src/HOL/Hoare_Parallel/OG_Syntax.thy
--- a/src/HOL/Hoare_Parallel/OG_Syntax.thy	Tue Aug 27 23:54:23 2013 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy	Wed Aug 28 00:18:50 2013 +0200
@@ -44,15 +44,15 @@
                     ("(0WHILE _ //DO _ /OD)"  [0, 0] 61)
 
 translations
-  "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond .{b}. c1 c2"
+  "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond \<lbrace>b\<rbrace> c1 c2"
   "IF b THEN c FI" \<rightleftharpoons> "IF b THEN c ELSE SKIP FI"
-  "WHILE b INV i DO c OD" \<rightharpoonup> "CONST While .{b}. i c"
+  "WHILE b INV i DO c OD" \<rightharpoonup> "CONST While \<lbrace>b\<rbrace> i c"
   "WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD"
 
-  "r IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST AnnCond1 r .{b}. c1 c2"
-  "r IF b THEN c FI" \<rightharpoonup> "CONST AnnCond2 r .{b}. c"
-  "r WHILE b INV i DO c OD" \<rightharpoonup> "CONST AnnWhile r .{b}. i c"
-  "r AWAIT b THEN c END" \<rightharpoonup> "CONST AnnAwait r .{b}. c"
+  "r IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST AnnCond1 r \<lbrace>b\<rbrace> c1 c2"
+  "r IF b THEN c FI" \<rightharpoonup> "CONST AnnCond2 r \<lbrace>b\<rbrace> c"
+  "r WHILE b INV i DO c OD" \<rightharpoonup> "CONST AnnWhile r \<lbrace>b\<rbrace> i c"
+  "r AWAIT b THEN c END" \<rightharpoonup> "CONST AnnAwait r \<lbrace>b\<rbrace> c"
   "r \<langle>c\<rangle>" \<rightleftharpoons> "r AWAIT CONST True THEN c END"
   "r WAIT b END" \<rightleftharpoons> "r AWAIT b THEN SKIP END"
  
diff -r 07593a0a27f4 -r effd8fcabca2 src/HOL/Hoare_Parallel/Quote_Antiquote.thy
--- a/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Tue Aug 27 23:54:23 2013 +0200
+++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Wed Aug 28 00:18:50 2013 +0200
@@ -6,13 +6,10 @@
 syntax
   "_quote"     :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"                ("(\<guillemotleft>_\<guillemotright>)" [0] 1000)
   "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"                ("\<acute>_" [1000] 1000)
-  "_Assert"    :: "'a \<Rightarrow> 'a set"                    ("(.{_}.)" [0] 1000)
-
-syntax (xsymbols)
-  "_Assert"    :: "'a \<Rightarrow> 'a set"            ("(\<lbrace>_\<rbrace>)" [0] 1000)
+  "_Assert"    :: "'a \<Rightarrow> 'a set"                    ("(\<lbrace>_\<rbrace>)" [0] 1000)
 
 translations
-  ".{b}." \<rightharpoonup> "CONST Collect \<guillemotleft>b\<guillemotright>"
+  "\<lbrace>b\<rbrace>" \<rightharpoonup> "CONST Collect \<guillemotleft>b\<guillemotright>"
 
 parse_translation {*
   let
diff -r 07593a0a27f4 -r effd8fcabca2 src/HOL/Hoare_Parallel/RG_Syntax.thy
--- a/src/HOL/Hoare_Parallel/RG_Syntax.thy	Tue Aug 27 23:54:23 2013 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy	Wed Aug 28 00:18:50 2013 +0200
@@ -20,10 +20,10 @@
 
 translations
   "\<acute>x := a" \<rightharpoonup> "CONST Basic \<guillemotleft>\<acute>(_update_name x (\<lambda>_. a))\<guillemotright>"
-  "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond .{b}. c1 c2"
+  "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond \<lbrace>b\<rbrace> c1 c2"
   "IF b THEN c FI" \<rightleftharpoons> "IF b THEN c ELSE SKIP FI"
-  "WHILE b DO c OD" \<rightharpoonup> "CONST While .{b}. c"
-  "AWAIT b THEN c END" \<rightleftharpoons> "CONST Await .{b}. c"
+  "WHILE b DO c OD" \<rightharpoonup> "CONST While \<lbrace>b\<rbrace> c"
+  "AWAIT b THEN c END" \<rightleftharpoons> "CONST Await \<lbrace>b\<rbrace> c"
   "\<langle>c\<rangle>" \<rightleftharpoons> "AWAIT CONST True THEN c END"
   "WAIT b END" \<rightleftharpoons> "AWAIT b THEN SKIP END"