author | regensbu |
Fri, 06 Oct 1995 16:17:08 +0100 | |
changeset 1273 | 6960ec882bca |
parent 1264 | 3eb91524b938 |
child 1370 | 7361ac9b024d |
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 + consts lfp :: "['a set=>'a set] => 'a set" defs (*least fixed point*) lfp_def "lfp(f) == Inter({u. f(u) <= u})" end