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)