changeset 923 | ff1574a81019 |
child 1114 | c8dfb56a7e95 |
922:196ca0973a6d | 923:ff1574a81019 |
---|---|
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 = mono + |
|
10 consts lfp :: "['a set=>'a set] => 'a set" |
|
11 defs |
|
12 (*least fixed point*) |
|
13 lfp_def "lfp(f) == Inter({u. f(u) <= u})" |
|
14 end |