author  clasohm 
Thu, 16 Sep 1993 12:20:38 +0200  
changeset 0  a5a9c433f639 
child 1474  3f7d67927fe2 
permissions  rwrr 
0  1 
(* Title: HOL/lfp.thy 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1992 University of Cambridge 

5 

6 
The KnasterTarski Theorem 

7 
*) 

8 

9 
Lfp = Set + 

10 
consts lfp :: "['a set=>'a set] => 'a set" 

11 
rules 

12 
(*least fixed point*) 

13 
lfp_def "lfp(f) == Inter({u. f(u) <= u})" 

14 
end 