--- a/src/HOL/Hoare/Hoare_Logic.thy Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/Hoare/Hoare_Logic.thy Thu Feb 15 12:11:00 2018 +0100
@@ -40,7 +40,7 @@
"Sem (IF b THEN c1 ELSE c2 FI) s s'"
definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
- where "Valid p c q \<longleftrightarrow> (!s s'. Sem c s s' --> s : p --> s' : q)"
+ where "Valid p c q \<longleftrightarrow> (\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> p \<longrightarrow> s' \<in> q)"
syntax