--- a/Paper/Paper.thy	Wed Jan 30 02:29:47 2013 +0000
+++ b/Paper/Paper.thy	Wed Jan 30 03:33:05 2013 +0000
@@ -118,10 +118,10 @@
 done 
 
 lemmas HR1 = 
-  Hoare_plus_halt_simple[where ?P1.0="P" and ?P2.0="Q" and ?P3.0="R\<iota>" and ?A="p\<^isub>1" and B="p\<^isub>2"]
+  Hoare_plus_halt[where ?S.0="R\<iota>" and ?A="p\<^isub>1" and B="p\<^isub>2"]
 
 lemmas HR2 =
-  Hoare_plus_unhalt_simple[where ?P1.0="P" and ?P2.0="Q" and ?A="p\<^isub>1" and B="p\<^isub>2"]
+  Hoare_plus_unhalt[where ?A="p\<^isub>1" and B="p\<^isub>2"]
 
 lemma inv_begin01:
   assumes "n > 1"
@@ -765,6 +765,14 @@
   \end{center}
   
   \noindent
+  For our Hoare-triples we can easily prove the following consequence rule
+
+  \begin{equation}
+  @{thm[mode=Rule] Hoare_consequence}
+  \end{equation}
+
+
+  \noindent
   Like Asperti and Ricciotti with their notion of realisability, we
   have set up our Hoare-rules so that we can deal explicitly
   with total correctness and non-terminantion, rather than have
@@ -928,7 +936,7 @@
 
 
   \begin{center}
-  @{thm haltP_def[where lm="ns"]}
+  @{thm haltP_def}
   \end{center}