equal
deleted
inserted
replaced
20 chain_finite :: "'a=>bool" |
20 chain_finite :: "'a=>bool" |
21 is_flat :: "'a=>bool" |
21 is_flat :: "'a=>bool" |
22 |
22 |
23 defs |
23 defs |
24 |
24 |
25 iterate_def "iterate n F c == nat_rec n c (%n x.F`x)" |
25 iterate_def "iterate n F c == nat_rec c (%n x.F`x) n" |
26 Ifix_def "Ifix F == lub(range(%i.iterate i F UU))" |
26 Ifix_def "Ifix F == lub(range(%i.iterate i F UU))" |
27 fix_def "fix == (LAM f. Ifix f)" |
27 fix_def "fix == (LAM f. Ifix f)" |
28 |
28 |
29 adm_def "adm P == !Y. is_chain(Y) --> |
29 adm_def "adm P == !Y. is_chain(Y) --> |
30 (!i.P(Y i)) --> P(lub(range Y))" |
30 (!i.P(Y i)) --> P(lub(range Y))" |