author | paulson |
Thu, 07 Oct 2004 15:42:30 +0200 | |
changeset 15234 | ec91a90c604e |
parent 15140 | 322485b816ac |
child 15386 | 06757406d8cf |
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 imports Product_Type begin constdefs lfp :: "['a set \<Rightarrow> 'a set] \<Rightarrow> 'a set" "lfp(f) == Inter({u. f(u) <= u})" (*least fixed point*) end