--- a/src/HOL/HOLCF/IOA/Pred.thy Sun Jan 10 23:25:11 2016 +0100
+++ b/src/HOL/HOLCF/IOA/Pred.thy Mon Jan 11 00:04:23 2016 +0100
@@ -12,14 +12,14 @@
type_synonym 'a predicate = "'a \<Rightarrow> bool"
-definition satisfies :: "'a \<Rightarrow> 'a predicate \<Rightarrow> bool" ("_ \<Turnstile> _" [100,9] 8)
+definition satisfies :: "'a \<Rightarrow> 'a predicate \<Rightarrow> bool" ("_ \<Turnstile> _" [100, 9] 8)
where "(s \<Turnstile> P) \<longleftrightarrow> P s"
definition valid :: "'a predicate \<Rightarrow> bool" (* ("|-") *)
where "valid P \<longleftrightarrow> (\<forall>s. (s \<Turnstile> P))"
definition NOT :: "'a predicate \<Rightarrow> 'a predicate" ("\<^bold>\<not> _" [40] 40)
- where "NOT P s \<longleftrightarrow> ~ (P s)"
+ where "NOT P s \<longleftrightarrow> \<not> P s"
definition AND :: "'a predicate \<Rightarrow> 'a predicate \<Rightarrow> 'a predicate" (infixr "\<^bold>\<and>" 35)
where "(P \<^bold>\<and> Q) s \<longleftrightarrow> P s \<and> Q s"