Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed proof (cf. d1d4d7a08a66);
authorwenzelm
Sun, 18 Oct 2009 22:19:05 +0200
changeset 32997 e760950ba6c5
parent 32996 d2e48879e65a
child 32998 31b19fa0de0b
child 33005 bd8e15958708
fixed proof (cf. d1d4d7a08a66);
src/HOLCF/Universal.thy file | annotate | diff | comparison | revisions 
--- a/src/HOLCF/Universal.thy	Sun Oct 18 22:16:37 2009 +0200
+++ b/src/HOLCF/Universal.thy	Sun Oct 18 22:19:05 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_f [where f=basis_emb])
+ apply (subst f_inv_onto_f [where f=basis_emb])
   apply (rule ubasis_until)
   apply (rule range_eqI [where x=compact_bot])
   apply simp
isabelle