changeset 0 | a5a9c433f639 |
child 1474 | 3f7d67927fe2 |
-1:000000000000 | 0:a5a9c433f639 |
---|---|
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 Knaster-Tarski 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 |