--- a/thys/Hoare_gen.thy	Thu Mar 27 13:06:27 2014 +0000
+++ b/thys/Hoare_gen.thy	Thu Mar 27 15:12:33 2014 +0000
@@ -203,6 +203,8 @@
   shows "((EXS x. P(x)) \<and>* r) s"
   by (metis assms pred_ex_def sep_globalise)
 
+
+(* Interpreted Hoare triples *)
 definition
   IHoare :: "('b::sep_algebra \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)  \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" 
              ("(1_).(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50)