author | haftmann |
Fri, 23 Oct 2009 10:08:29 +0200 | |
changeset 33080 | 180feec9acf6 |
parent 33079 | 06a48bbeb22a |
child 33081 | fe29679cabc2 |
--- a/src/HOLCF/Universal.thy Thu Oct 22 16:58:22 2009 +0200 +++ b/src/HOLCF/Universal.thy Fri Oct 23 10:08:29 2009 +0200 @@ -805,7 +805,7 @@ lemma basis_emb_prj_less: "ubasis_le (basis_emb (basis_prj x)) x" unfolding basis_prj_def - apply (subst f_inv_onto_f [where f=basis_emb]) + apply (subst f_inv_into_f [where f=basis_emb]) apply (rule ubasis_until) apply (rule range_eqI [where x=compact_bot]) apply simp