equal
deleted
inserted
replaced
4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 Greatest fixed points (requires Lfp too!) |
6 Greatest fixed points (requires Lfp too!) |
7 *) |
7 *) |
8 |
8 |
9 theory Gfp = Lfp: |
9 theory Gfp |
|
10 import Lfp |
|
11 begin |
10 |
12 |
11 constdefs |
13 constdefs |
12 gfp :: "['a set=>'a set] => 'a set" |
14 gfp :: "['a set=>'a set] => 'a set" |
13 "gfp(f) == Union({u. u <= f(u)})" (*greatest fixed point*) |
15 "gfp(f) == Union({u. u <= f(u)})" (*greatest fixed point*) |
14 |
16 |