# HG changeset patch
# User nipkow
# Date 759618426 -3600
# Node ID 0d0a6a17a02f6ca1f33375bf7626dcfe44f027bf
# Parent  bc10568855ee1c16b641f80dd0fdecb784d710f5
case was renamed to sum_case

diff -r bc10568855ee -r 0d0a6a17a02f src/HOLCF/Lift1.ML
--- a/src/HOLCF/Lift1.ML	Mon Jan 24 12:03:53 1994 +0100
+++ b/src/HOLCF/Lift1.ML	Wed Jan 26 22:07:06 1994 +0100
@@ -71,7 +71,7 @@
  (fn prems =>
 	[
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
-	(rtac (case_Inl RS ssubst) 1),
+	(rtac (sum_case_Inl RS ssubst) 1),
 	(rtac refl 1)
 	]);
 
@@ -80,7 +80,7 @@
  (fn prems =>
 	[
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
-	(rtac (case_Inr RS ssubst) 1),
+	(rtac (sum_case_Inr RS ssubst) 1),
 	(rtac refl 1)
 	]);
 
@@ -91,7 +91,7 @@
  (fn prems =>
 	[
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
-	(rtac (case_Inl RS ssubst) 1),
+	(rtac (sum_case_Inl RS ssubst) 1),
 	(rtac TrueI 1)
 	]);
 
@@ -104,8 +104,8 @@
 	(atac 2),
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
-	(rtac (case_Inr RS ssubst) 1),
-	(rtac (case_Inl RS ssubst) 1),
+	(rtac (sum_case_Inr RS ssubst) 1),
+	(rtac (sum_case_Inl RS ssubst) 1),
 	(rtac refl 1)
 	]);
 
@@ -115,8 +115,8 @@
 	[
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
-	(rtac (case_Inr RS ssubst) 1),
-	(rtac (case_Inr RS ssubst) 1),
+	(rtac (sum_case_Inr RS ssubst) 1),
+	(rtac (sum_case_Inr RS ssubst) 1),
 	(rtac refl 1)
 	]);
 
diff -r bc10568855ee -r 0d0a6a17a02f src/HOLCF/Lift1.thy
--- a/src/HOLCF/Lift1.thy	Mon Jan 24 12:03:53 1994 +0100
+++ b/src/HOLCF/Lift1.thy	Wed Jan 26 22:07:06 1994 +0100
@@ -40,14 +40,14 @@
   Iup_def       "Iup(x)  == Abs_Lift(Inr(x))"
 
   Ilift_def     "Ilift(f)(x)==\
-\                case  (Rep_Lift(x)) (%y.UU) (%z.f[z])"
+\                sum_case  (Rep_Lift(x)) (%y.UU) (%z.f[z])"
  
   less_lift_def "less_lift(x1)(x2) == \
-\          (case (Rep_Lift(x1))\
-\                (% y1.True)\
-\                (% y2.case (Rep_Lift(x2))\
-\                           (% z1.False)\
-\                           (% z2.y2<<z2)))"
+\          (sum_case (Rep_Lift(x1))\
+\                    (% y1.True)\
+\                    (% y2.sum_case (Rep_Lift(x2))\
+\                                   (% z1.False)\
+\                                   (% z2.y2<<z2)))"
 
 end
 
diff -r bc10568855ee -r 0d0a6a17a02f src/HOLCF/lift1.ML
--- a/src/HOLCF/lift1.ML	Mon Jan 24 12:03:53 1994 +0100
+++ b/src/HOLCF/lift1.ML	Wed Jan 26 22:07:06 1994 +0100
@@ -71,7 +71,7 @@
  (fn prems =>
 	[
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
-	(rtac (case_Inl RS ssubst) 1),
+	(rtac (sum_case_Inl RS ssubst) 1),
 	(rtac refl 1)
 	]);
 
@@ -80,7 +80,7 @@
  (fn prems =>
 	[
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
-	(rtac (case_Inr RS ssubst) 1),
+	(rtac (sum_case_Inr RS ssubst) 1),
 	(rtac refl 1)
 	]);
 
@@ -91,7 +91,7 @@
  (fn prems =>
 	[
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
-	(rtac (case_Inl RS ssubst) 1),
+	(rtac (sum_case_Inl RS ssubst) 1),
 	(rtac TrueI 1)
 	]);
 
@@ -104,8 +104,8 @@
 	(atac 2),
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
-	(rtac (case_Inr RS ssubst) 1),
-	(rtac (case_Inl RS ssubst) 1),
+	(rtac (sum_case_Inr RS ssubst) 1),
+	(rtac (sum_case_Inl RS ssubst) 1),
 	(rtac refl 1)
 	]);
 
@@ -115,8 +115,8 @@
 	[
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
 	(rtac (Abs_Lift_inverse RS ssubst) 1),
-	(rtac (case_Inr RS ssubst) 1),
-	(rtac (case_Inr RS ssubst) 1),
+	(rtac (sum_case_Inr RS ssubst) 1),
+	(rtac (sum_case_Inr RS ssubst) 1),
 	(rtac refl 1)
 	]);
 
diff -r bc10568855ee -r 0d0a6a17a02f src/HOLCF/lift1.thy
--- a/src/HOLCF/lift1.thy	Mon Jan 24 12:03:53 1994 +0100
+++ b/src/HOLCF/lift1.thy	Wed Jan 26 22:07:06 1994 +0100
@@ -40,14 +40,14 @@
   Iup_def       "Iup(x)  == Abs_Lift(Inr(x))"
 
   Ilift_def     "Ilift(f)(x)==\
-\                case  (Rep_Lift(x)) (%y.UU) (%z.f[z])"
+\                sum_case  (Rep_Lift(x)) (%y.UU) (%z.f[z])"
  
   less_lift_def "less_lift(x1)(x2) == \
-\          (case (Rep_Lift(x1))\
-\                (% y1.True)\
-\                (% y2.case (Rep_Lift(x2))\
-\                           (% z1.False)\
-\                           (% z2.y2<<z2)))"
+\          (sum_case (Rep_Lift(x1))\
+\                    (% y1.True)\
+\                    (% y2.sum_case (Rep_Lift(x2))\
+\                                   (% z1.False)\
+\                                   (% z2.y2<<z2)))"
 
 end