changeset 0 | a5a9c433f639 |
child 1474 | 3f7d67927fe2 |
-1:000000000000 | 0:a5a9c433f639 |
---|---|
1 (* Title: HOL/gfp.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 Greatest fixed points |
|
7 *) |
|
8 |
|
9 Gfp = Lfp + |
|
10 consts gfp :: "['a set=>'a set] => 'a set" |
|
11 rules |
|
12 (*greatest fixed point*) |
|
13 gfp_def "gfp(f) == Union({u. u <= f(u)})" |
|
14 end |