author  wenzelm 
Sat, 17 Sep 2005 17:35:26 +0200  
changeset 17456  bcf7544875b2 
parent 1474  3f7d67927fe2 
child 20140  98acc6d0fab6 
permissions  rwrr 
17456  1 
(* Title: CCL/Lfp.thy 
0  2 
ID: $Id$ 
1474  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1992 University of Cambridge 
5 
*) 

6 

17456  7 
header {* The KnasterTarski Theorem *} 
8 

9 
theory Lfp 

10 
imports Set 

11 
uses "subset.ML" "equalities.ML" "mono.ML" 

12 
begin 

13 

14 
constdefs 

15 
lfp :: "['a set=>'a set] => 'a set" (*least fixed point*) 

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

17 

18 
ML {* use_legacy_bindings (the_context ()) *} 

19 

0  20 
end 