diff -r f8b2bf858caf -r 457240e42972 thys/Hoare_gen.thy
--- a/thys/Hoare_gen.thy	Thu Mar 27 11:50:37 2014 +0000
+++ b/thys/Hoare_gen.thy	Thu Mar 27 13:06:27 2014 +0000
@@ -30,20 +30,26 @@
 
 lemmas sep_conj_cond = sep_conj_cond1 sep_conj_cond2 sep_conj_cond3
 
-lemma cond_true_eq[simp]: "<True> = \<box>"
+lemma cond_true_eq [simp]: 
+  "<True> = \<box>"
   by(unfold sep_empty_def pasrt_def, auto)
 
-lemma cond_true_eq1: "(<True> \<and>* p) = p"
-  by(simp)
+lemma cond_true_eq1: 
+  "(<True> \<and>* p) = p"
+  by (simp)
 
-lemma false_simp [simp]: "<False> = sep_false" (* move *)
+lemma cond_true_eq2: 
+  "(p \<and>* <True>) = p"
+  by simp
+
+lemma false_simp [simp]: 
+  "<False> = sep_false" (* move *)
   by (simp add:pasrt_def)
 
-lemma cond_true_eq2: "(p \<and>* <True>) = p"
-  by simp
-
-lemma condD: "(<b> \<and>* r) s \<Longrightarrow> b \<and> r s" 
-by (unfold sep_conj_def pasrt_def, auto)
+lemma condD: 
+  "(<b> \<and>* r) s \<Longrightarrow> b \<and> r s" 
+unfolding sep_conj_def pasrt_def
+by auto
 
 locale sep_exec = 
    fixes step :: "'conf \<Rightarrow> 'conf"
@@ -189,8 +195,8 @@
 
 lemma hoare_sep_false: 
   "\<lbrace>sep_false\<rbrace> c \<lbrace>q\<rbrace>" 
-  by(unfold Hoare_gen_def, clarify, simp)
-
+unfolding Hoare_gen_def
+by auto
 
 lemma pred_exI: 
   assumes "(P(x) \<and>* r) s"