author | nipkow |
Fri, 24 Nov 2000 16:49:27 +0100 | |
changeset 10519 | ade64af4c57c |
parent 10212 | 33fe2d701ddd |
child 11609 | 3f3d1add4d94 |
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 + Product_Type + constdefs lfp :: ['a set=>'a set] => 'a set "lfp(f) == Inter({u. f(u) <= u})" (*least fixed point*) end