Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HOLCF/Powerdomains.thy
changeset 41436 480978f80eae
parent 41292 2b7bc8d9fd6e
child 42151 4da4fc77664b 
--- a/src/HOL/HOLCF/Powerdomains.thy	Thu Jan 06 21:06:18 2011 +0100
+++ b/src/HOL/HOLCF/Powerdomains.thy	Thu Jan 06 16:52:35 2011 -0800
@@ -78,7 +78,7 @@
   "(liftprj :: udom u \<rightarrow> 'a upper_pd u) = u_map\<cdot>prj"
 
 definition
-  "liftdefl (t::'a upper_pd itself) = pdefl\<cdot>DEFL('a upper_pd)"
+  "liftdefl (t::'a upper_pd itself) = liftdefl_of\<cdot>DEFL('a upper_pd)"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)"
@@ -111,7 +111,7 @@
   "(liftprj :: udom u \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj"
 
 definition
-  "liftdefl (t::'a lower_pd itself) = pdefl\<cdot>DEFL('a lower_pd)"
+  "liftdefl (t::'a lower_pd itself) = liftdefl_of\<cdot>DEFL('a lower_pd)"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)"
@@ -144,7 +144,7 @@
   "(liftprj :: udom u \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj"
 
 definition
-  "liftdefl (t::'a convex_pd itself) = pdefl\<cdot>DEFL('a convex_pd)"
+  "liftdefl (t::'a convex_pd itself) = liftdefl_of\<cdot>DEFL('a convex_pd)"
 
 instance proof
   show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)"
isabelle