# HG changeset patch
# User huffman
# Date 1213997844 -7200
# Node ID aa28b1d33866b7565a7aec9ec1380f4b463c134b
# Parent  d0229bc6c46113cf6f4062cb803ad6408ad20093
remove unused constant liftpair

diff -r d0229bc6c461 -r aa28b1d33866 src/HOLCF/Lift.thy
--- 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}. *}