# HG changeset patch
# User nipkow
# Date 1370598712 -7200
# Node ID 427fa76ea7276450da14a7eccdb1f8b75c667a76
# Parent  8ce7fba90bb39beae0b5be8a4ebfbe158b75ef2a
tuned

diff -r 8ce7fba90bb3 -r 427fa76ea727 src/HOL/IMP/VCG.thy
--- 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)