equal
deleted
inserted
replaced
18 adm :: "('a::cpo=>bool)=>bool" |
18 adm :: "('a::cpo=>bool)=>bool" |
19 admw :: "('a=>bool)=>bool" |
19 admw :: "('a=>bool)=>bool" |
20 |
20 |
21 primrec |
21 primrec |
22 iterate_0 "iterate 0 F x = x" |
22 iterate_0 "iterate 0 F x = x" |
23 iterate_Suc "iterate (Suc n) F x = F`(iterate n F x)" |
23 iterate_Suc "iterate (Suc n) F x = F$(iterate n F x)" |
24 |
24 |
25 defs |
25 defs |
26 |
26 |
27 Ifix_def "Ifix F == lub(range(%i. iterate i F UU))" |
27 Ifix_def "Ifix F == lub(range(%i. iterate i F UU))" |
28 fix_def "fix == (LAM f. Ifix f)" |
28 fix_def "fix == (LAM f. Ifix f)" |