# HG changeset patch
# User nipkow
# Date 1369638926 -7200
# Node ID 31bd65d96f4d14e8909f3df03851d5122d0bd2e8
# Parent  3c22e72603b3934db0fcbb274214c56ce63eb622
tuned

diff -r 3c22e72603b3 -r 31bd65d96f4d src/HOL/IMP/Hoare.thy
--- a/src/HOL/IMP/Hoare.thy	Mon May 27 07:44:10 2013 +0200
+++ b/src/HOL/IMP/Hoare.thy	Mon May 27 09:15:26 2013 +0200
@@ -10,7 +10,7 @@
 
 definition
 hoare_valid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" 50) where
-"\<Turnstile> {P}c{Q} = (\<forall>s t. (c,s) \<Rightarrow> t  \<longrightarrow>  P s \<longrightarrow>  Q t)"
+"\<Turnstile> {P}c{Q} = (\<forall>s t. P s \<and> (c,s) \<Rightarrow> t  \<longrightarrow>  Q t)"
 
 abbreviation state_subst :: "state \<Rightarrow> aexp \<Rightarrow> vname \<Rightarrow> state"
   ("_[_'/_]" [1000,0,0] 999)