| changeset 62020 | 5d208fd2507d |
| parent 60770 | 240563fbf41d |
| child 67443 | 3abf6a722518 |
--- a/src/CCL/Lfp.thy Thu Dec 31 21:46:31 2015 +0100 +++ b/src/CCL/Lfp.thy Fri Jan 01 10:49:00 2016 +0100 @@ -10,7 +10,7 @@ begin definition - lfp :: "['a set\<Rightarrow>'a set] \<Rightarrow> 'a set" where -- "least fixed point" + lfp :: "['a set\<Rightarrow>'a set] \<Rightarrow> 'a set" where \<comment> "least fixed point" "lfp(f) == Inter({u. f(u) <= u})" (* lfp(f) is the greatest lower bound of {u. f(u) <= u} *)