Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HOLCF/IOA/Pred.thy
changeset 74101 d804e93ae9ff
parent 62194 0aabc5931361 
--- a/src/HOL/HOLCF/IOA/Pred.thy	Sun Aug 01 23:18:13 2021 +0200
+++ b/src/HOL/HOLCF/IOA/Pred.thy	Mon Aug 02 10:01:06 2021 +0000
@@ -18,8 +18,8 @@
 definition valid :: "'a predicate \<Rightarrow> bool"  ("\<TTurnstile> _" [9] 8)
   where "(\<TTurnstile> P) \<longleftrightarrow> (\<forall>s. (s \<Turnstile> P))"
 
-definition NOT :: "'a predicate \<Rightarrow> 'a predicate"  ("\<^bold>\<not> _" [40] 40)
-  where "NOT P s \<longleftrightarrow> \<not> P s"
+definition Not :: "'a predicate \<Rightarrow> 'a predicate"  ("\<^bold>\<not> _" [40] 40)
+  where NOT_def: "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"
isabelle