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)"```