diff -r 67f6044c1891 -r 1ff571813848 src/HOLCF/Fix.thy --- a/src/HOLCF/Fix.thy Tue Jun 14 04:04:09 2005 +0200 +++ b/src/HOLCF/Fix.thy Tue Jun 14 04:05:15 2005 +0200 @@ -100,7 +100,7 @@ by (induct_tac n, simp_all) lemma cont_iterate: "cont (iterate n)" -by (rule cont_iterate1 [THEN cont2cont_CF1L_rev2]) +by (rule cont_iterate1 [THEN cont2cont_lambda]) lemmas monofun_iterate2 = cont_iterate2 [THEN cont2mono, standard] lemmas contlub_iterate2 = cont_iterate2 [THEN cont2contlub, standard]