equal
deleted
inserted
replaced
922 by (stac contlub_cfun_fun 1); |
922 by (stac contlub_cfun_fun 1); |
923 by (rtac chain_iterate 1); |
923 by (rtac chain_iterate 1); |
924 by (stac contlub_cfun_fun 1); |
924 by (stac contlub_cfun_fun 1); |
925 by (rtac chain_iterate 1); |
925 by (rtac chain_iterate 1); |
926 by (rtac lub_mono 1); |
926 by (rtac lub_mono 1); |
927 by (rtac (chain_iterate RS ch2ch_fappL) 1); |
927 by (rtac (chain_iterate RS ch2ch_Rep_CFunL) 1); |
928 by (rtac (chain_iterate RS ch2ch_fappL) 1); |
928 by (rtac (chain_iterate RS ch2ch_Rep_CFunL) 1); |
929 by (rtac allI 1); |
929 by (rtac allI 1); |
930 by (resolve_tac prems 1); |
930 by (resolve_tac prems 1); |
931 qed"take_lemma_less1"; |
931 qed"take_lemma_less1"; |
932 |
932 |
933 |
933 |