src/HOL/HOLCF/IOA/Pred.thy

 
 default_sort type
 
 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"
 
 definition OR :: "'a predicate \<Rightarrow> 'a predicate \<Rightarrow> 'a predicate"  (infixr "\<^bold>\<or>" 30)