--- a/src/ZF/Fixedpt.thy Tue Sep 27 16:51:35 2022 +0100
+++ b/src/ZF/Fixedpt.thy Tue Sep 27 17:03:23 2022 +0100
@@ -10,7 +10,7 @@
definition
(*monotone operator from Pow(D) to itself*)
bnd_mono :: "[i,i=>i]=>o" where
- "bnd_mono(D,h) \<equiv> h(D)<=D & (\<forall>W X. W<=X \<longrightarrow> X<=D \<longrightarrow> h(W) \<subseteq> h(X))"
+ "bnd_mono(D,h) \<equiv> h(D)<=D \<and> (\<forall>W X. W<=X \<longrightarrow> X<=D \<longrightarrow> h(W) \<subseteq> h(X))"
definition
lfp :: "[i,i=>i]=>i" where