diff -r ceb0bdc99893 -r 6c722e960f2e thys/Hoare_gen.thy
--- a/thys/Hoare_gen.thy	Fri Mar 21 21:40:51 2014 +0800
+++ b/thys/Hoare_gen.thy	Fri Mar 21 13:49:20 2014 +0000
@@ -12,7 +12,7 @@
 where "pasrt b = (\<lambda> s . s = 0 \<and> b)"
 
 
-(* smae as sep.mult.left_commute *)
+(* same as sep.mult.left_commute *)
 lemma sep_conj_cond1: 
   "(p \<and>* <cond> \<and>* q) = (<cond> \<and>* p \<and>* q)"
   by (rule sep.mult.left_commute)
@@ -289,15 +289,15 @@
 by (smt IHoare_def code_exI)
 
 lemma I_code_extension: 
-  assumes h: "I. \<lbrace> P \<rbrace> c \<lbrace> Q \<rbrace>"
-  shows "I. \<lbrace> P \<rbrace> c ** e \<lbrace> Q \<rbrace>"
+  assumes h: "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>"
+  shows "I. \<lbrace>P\<rbrace> c \<and>* e \<lbrace>Q\<rbrace>"
   using h
   by (smt IHoare_def sep_exec.code_extension)
 
 lemma I_composition: 
   assumes h1: "I. \<lbrace>P\<rbrace> c1 \<lbrace>Q\<rbrace>"
     and h2: "I. \<lbrace>Q\<rbrace> c2 \<lbrace>R\<rbrace>"
-  shows "I. \<lbrace>P\<rbrace> c1 ** c2 \<lbrace>R\<rbrace>"
+  shows "I. \<lbrace>P\<rbrace> c1 \<and>* c2 \<lbrace>R\<rbrace>"
   using h1 h2
 by (smt IHoare_def sep_exec.composition)