--- a/src/HOLCF/Lift.thy Fri Jun 20 23:01:09 2008 +0200
+++ b/src/HOLCF/Lift.thy Fri Jun 20 23:37:24 2008 +0200
@@ -6,7 +6,7 @@
header {* Lifting types of class type to flat pcpo's *}
theory Lift
-imports Discrete Up Cprod Countable
+imports Discrete Up Countable
begin
defaultsort type
@@ -110,10 +110,6 @@
flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where
"flift2 f = (FLIFT x. Def (f x))"
-definition
- liftpair :: "'a lift \<times> 'b lift \<Rightarrow> ('a \<times> 'b) lift" where
- "liftpair x = csplit\<cdot>(FLIFT x y. Def (x, y))\<cdot>x"
-
subsection {* Continuity Proofs for flift1, flift2 *}
text {* Need the instance of @{text flat}. *}