equal
deleted
inserted
replaced
914 apply (subst contlub_cfun_fun) |
914 apply (subst contlub_cfun_fun) |
915 apply (rule chain_iterate) |
915 apply (rule chain_iterate) |
916 apply (rule lub_mono) |
916 apply (rule lub_mono) |
917 apply (rule chain_iterate [THEN ch2ch_Rep_CFunL]) |
917 apply (rule chain_iterate [THEN ch2ch_Rep_CFunL]) |
918 apply (rule chain_iterate [THEN ch2ch_Rep_CFunL]) |
918 apply (rule chain_iterate [THEN ch2ch_Rep_CFunL]) |
919 apply (rule allI) |
|
920 apply (rule prems [unfolded seq.take_def]) |
919 apply (rule prems [unfolded seq.take_def]) |
921 done |
920 done |
922 |
921 |
923 |
922 |
924 lemma take_lemma_less: "(!n. seq_take n$x << seq_take n$x') = (x << x')" |
923 lemma take_lemma_less: "(!n. seq_take n$x << seq_take n$x') = (x << x')" |