author | wenzelm |
Sat, 05 Jun 2004 13:07:04 +0200 | |
changeset 14872 | 3f2144aebd76 |
parent 14169 | 0590de71a016 |
child 15131 | c69542757a4d |
permissions | -rw-r--r-- |
(* Title: HOL/Lfp.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge The Knaster-Tarski Theorem *) theory Lfp = Product_Type: constdefs lfp :: "['a set \<Rightarrow> 'a set] \<Rightarrow> 'a set" "lfp(f) == Inter({u. f(u) <= u})" (*least fixed point*) end