tuned

--- a/src/HOL/IMP/VCG.thy	Fri Jun 07 09:28:59 2013 +0200
+++ b/src/HOL/IMP/VCG.thy	Fri Jun 07 11:51:52 2013 +0200
@@ -65,7 +65,7 @@
 qed (auto intro: hoare.conseq)
 
 corollary vc_sound':
-  "(\<forall>s. vc c Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c Q s) \<Longrightarrow> \<turnstile> {P} strip c {Q}"
+  "\<lbrakk> \<forall>s. vc c Q s; \<forall>s. P s \<longrightarrow> pre c Q s \<rbrakk> \<Longrightarrow> \<turnstile> {P} strip c {Q}"
 by (metis strengthen_pre vc_sound)