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/Gfp.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 {* Greatest fixed points *} 
8 

9 
theory Gfp 

10 
imports Lfp 

11 
begin 

12 

13 
constdefs 

14 
gfp :: "['a set=>'a set] => 'a set" (*greatest fixed point*) 

15 
"gfp(f) == Union({u. u <= f(u)})" 

16 

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

18 

0  19 
end 