changeset 67443 | 3abf6a722518 |
parent 62020 | 5d208fd2507d |
--- a/src/CCL/Gfp.thy Tue Jan 16 09:12:16 2018 +0100 +++ b/src/CCL/Gfp.thy Tue Jan 16 09:30:00 2018 +0100 @@ -10,7 +10,7 @@ begin definition - gfp :: "['a set\<Rightarrow>'a set] \<Rightarrow> 'a set" where \<comment> "greatest fixed point" + gfp :: "['a set\<Rightarrow>'a set] \<Rightarrow> 'a set" where \<comment> \<open>greatest fixed point\<close> "gfp(f) == Union({u. u <= f(u)})" (* gfp(f) is the least upper bound of {u. u <= f(u)} *)