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/ZF/UNITY/Monotonicity.thy
changeset 76214 0c18df79b1c8
parent 76213 e44d86131648
child 76215 a642599ffdea 
--- a/src/ZF/UNITY/Monotonicity.thy	Tue Sep 27 16:51:35 2022 +0100
+++ b/src/ZF/UNITY/Monotonicity.thy	Tue Sep 27 17:03:23 2022 +0100
@@ -14,7 +14,7 @@
 definition
   mono1 :: "[i, i, i, i, i=>i] => o"  where
   "mono1(A, r, B, s, f) \<equiv>
-    (\<forall>x \<in> A. \<forall>y \<in> A. <x,y> \<in> r \<longrightarrow> <f(x), f(y)> \<in> s) & (\<forall>x \<in> A. f(x) \<in> B)"
+    (\<forall>x \<in> A. \<forall>y \<in> A. <x,y> \<in> r \<longrightarrow> <f(x), f(y)> \<in> s) \<and> (\<forall>x \<in> A. f(x) \<in> B)"
 
   (* monotonicity of a 2-place meta-function f *)
 
@@ -22,7 +22,7 @@
   mono2 :: "[i, i, i, i, i, i, [i,i]=>i] => o"  where
   "mono2(A, r, B, s, C, t, f) \<equiv> 
     (\<forall>x \<in> A. \<forall>y \<in> A. \<forall>u \<in> B. \<forall>v \<in> B.
-              <x,y> \<in> r & <u,v> \<in> s \<longrightarrow> <f(x,u), f(y,v)> \<in> t) &
+              <x,y> \<in> r \<and> <u,v> \<in> s \<longrightarrow> <f(x,u), f(y,v)> \<in> t) \<and>
     (\<forall>x \<in> A. \<forall>y \<in> B. f(x,y) \<in> C)"
 
  (* Internalized relations on sets and multisets *)
isabelle