author | wenzelm |
Tue, 24 Nov 1998 12:03:09 +0100 | |
changeset 5953 | d6017ce6b93e |
parent 3947 | eb707467f8c5 |
child 8882 | 9df44a4f1bf7 |
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 *) Lfp = mono + Prod + global constdefs lfp :: ['a set=>'a set] => 'a set "lfp(f) == Inter({u. f(u) <= u})" (*least fixed point*) local end