equal
deleted
inserted
replaced
3 (* Loeckx & Sieber S.88 *) |
3 (* Loeckx & Sieber S.88 *) |
4 |
4 |
5 Goalw [Ifix_def] "Ifix F= lub (range (%i.%G. iterate i G UU)) F"; |
5 Goalw [Ifix_def] "Ifix F= lub (range (%i.%G. iterate i G UU)) F"; |
6 by (stac thelub_fun 1); |
6 by (stac thelub_fun 1); |
7 by (rtac refl 2); |
7 by (rtac refl 2); |
8 by (blast_tac (claset() addIs [ch2ch_fun, chainI, less_fun RS iffD2, |
8 by (blast_tac (claset() addIs [ch2ch_fun, chainI, expand_fun_less RS iffD2, |
9 chain_iterate RS chainE]) 1); |
9 chain_iterate RS chainE]) 1); |
10 qed "loeckx_sieber"; |
10 qed "loeckx_sieber"; |
11 |
11 |
12 (* |
12 (* |
13 |
13 |