# HG changeset patch
# User lcp
# Date 777207417 -7200
# Node ID 164be35c8a16964092adfd5d2fe53100248d9c85
# Parent  be4c4ba8714337653a029fc53dd0f48c5ec827eb
HOLCF/Lift1.thy: updated for new sum_case by using "case" syntax

diff -r be4c4ba87143 -r 164be35c8a16 src/HOLCF/Lift1.thy
--- a/src/HOLCF/Lift1.thy	Wed Aug 17 10:42:41 1994 +0200
+++ b/src/HOLCF/Lift1.thy	Thu Aug 18 12:56:57 1994 +0200
@@ -39,15 +39,15 @@
   UU_lift_def   "UU_lift == Abs_Lift(Inl(UU))"
   Iup_def       "Iup(x)  == Abs_Lift(Inr(x))"
 
-  Ilift_def     "Ilift(f)(x)==\
-\                sum_case  (Rep_Lift(x)) (%y.UU) (%z.f[z])"
+  Ilift_def     "Ilift(f)(x)== \
+\                case Rep_Lift(x) of Inl(y) => UU | Inr(z) => f[z]"
  
-  less_lift_def "less_lift(x1)(x2) == \
-\          (sum_case (Rep_Lift(x1))\
-\                    (% y1.True)\
-\                    (% y2.sum_case (Rep_Lift(x2))\
-\                                   (% z1.False)\
-\                                   (% z2.y2<<z2)))"
+  less_lift_def "less_lift(x1)(x2) == 		\
+\          (case Rep_Lift(x1) of 		\
+\               Inl(y1) => True 		\
+\             | Inr(y2) => 			\
+\                   (case Rep_Lift(x2) of Inl(z1) => False	\
+\                                       | Inr(z2) => y2<<z2))"
 
 end