# HG changeset patch
# User mueller
# Date 861896430 -7200
# Node ID 9c44acc3c6fa67424c41d091c5f9b5d06215b6dd
# Parent  50e14d6d894f9eb758b6d450b8a6261358f0e7e1
added liftpair definition

diff -r 50e14d6d894f -r 9c44acc3c6fa src/HOLCF/Lift3.thy
--- a/src/HOLCF/Lift3.thy	Thu Apr 24 17:38:33 1997 +0200
+++ b/src/HOLCF/Lift3.thy	Thu Apr 24 17:40:30 1997 +0200
@@ -1,6 +1,6 @@
 (*  Title:      HOLCF/Lift3.thy
     ID:         $Id$
-    Author:     Olaf Mueller, Robert Sandner
+    Author:     Olaf Mueller
     Copyright   1996 Technische Universitaet Muenchen
 
 Class Instance lift::(term)pcpo
@@ -12,20 +12,28 @@
 
 consts 
  flift1      :: "('a => 'b::pcpo) => ('a lift -> 'b)"
- flift2      :: "('a => 'b) => ('a lift -> 'b lift)"
+ flift2      :: "('a => 'b)       => ('a lift -> 'b lift)"
+
+ liftpair    ::"'a::term lift * 'b::term lift => ('a * 'b) lift"
 
 translations
  "UU" <= "Undef"
 
 defs
  flift1_def
-  "flift1 f  == (LAM x. (case x of 
+  "flift1 f == (LAM x. (case x of 
                    Undef => UU
                  | Def y => (f y)))"
  flift2_def
   "flift2 f == (LAM x. (case x of 
-                              Undef => Undef
-                            | Def y => Def (f y)))"
+                   Undef => UU
+                 | Def y => Def (f y)))"
+ liftpair_def
+  "liftpair x  == (case (cfst`x) of 
+                  Undef  => UU
+                | Def x1 => (case (csnd`x) of 
+                               Undef => UU
+                             | Def x2 => Def (x1,x2)))"
 
 end