case was renamed to sum_case
authornipkow
Wed Jan 26 22:07:06 1994 +0100 (1994-01-26)
changeset 2480d0a6a17a02f
parent 247 bc10568855ee
child 249 ec0b34154a6e
case was renamed to sum_case
src/HOLCF/Lift1.ML
src/HOLCF/Lift1.thy
src/HOLCF/lift1.ML
src/HOLCF/lift1.thy
     1.1 --- a/src/HOLCF/Lift1.ML	Mon Jan 24 12:03:53 1994 +0100
     1.2 +++ b/src/HOLCF/Lift1.ML	Wed Jan 26 22:07:06 1994 +0100
     1.3 @@ -71,7 +71,7 @@
     1.4   (fn prems =>
     1.5  	[
     1.6  	(rtac (Abs_Lift_inverse RS ssubst) 1),
     1.7 -	(rtac (case_Inl RS ssubst) 1),
     1.8 +	(rtac (sum_case_Inl RS ssubst) 1),
     1.9  	(rtac refl 1)
    1.10  	]);
    1.11  
    1.12 @@ -80,7 +80,7 @@
    1.13   (fn prems =>
    1.14  	[
    1.15  	(rtac (Abs_Lift_inverse RS ssubst) 1),
    1.16 -	(rtac (case_Inr RS ssubst) 1),
    1.17 +	(rtac (sum_case_Inr RS ssubst) 1),
    1.18  	(rtac refl 1)
    1.19  	]);
    1.20  
    1.21 @@ -91,7 +91,7 @@
    1.22   (fn prems =>
    1.23  	[
    1.24  	(rtac (Abs_Lift_inverse RS ssubst) 1),
    1.25 -	(rtac (case_Inl RS ssubst) 1),
    1.26 +	(rtac (sum_case_Inl RS ssubst) 1),
    1.27  	(rtac TrueI 1)
    1.28  	]);
    1.29  
    1.30 @@ -104,8 +104,8 @@
    1.31  	(atac 2),
    1.32  	(rtac (Abs_Lift_inverse RS ssubst) 1),
    1.33  	(rtac (Abs_Lift_inverse RS ssubst) 1),
    1.34 -	(rtac (case_Inr RS ssubst) 1),
    1.35 -	(rtac (case_Inl RS ssubst) 1),
    1.36 +	(rtac (sum_case_Inr RS ssubst) 1),
    1.37 +	(rtac (sum_case_Inl RS ssubst) 1),
    1.38  	(rtac refl 1)
    1.39  	]);
    1.40  
    1.41 @@ -115,8 +115,8 @@
    1.42  	[
    1.43  	(rtac (Abs_Lift_inverse RS ssubst) 1),
    1.44  	(rtac (Abs_Lift_inverse RS ssubst) 1),
    1.45 -	(rtac (case_Inr RS ssubst) 1),
    1.46 -	(rtac (case_Inr RS ssubst) 1),
    1.47 +	(rtac (sum_case_Inr RS ssubst) 1),
    1.48 +	(rtac (sum_case_Inr RS ssubst) 1),
    1.49  	(rtac refl 1)
    1.50  	]);
    1.51  
     2.1 --- a/src/HOLCF/Lift1.thy	Mon Jan 24 12:03:53 1994 +0100
     2.2 +++ b/src/HOLCF/Lift1.thy	Wed Jan 26 22:07:06 1994 +0100
     2.3 @@ -40,14 +40,14 @@
     2.4    Iup_def       "Iup(x)  == Abs_Lift(Inr(x))"
     2.5  
     2.6    Ilift_def     "Ilift(f)(x)==\
     2.7 -\                case  (Rep_Lift(x)) (%y.UU) (%z.f[z])"
     2.8 +\                sum_case  (Rep_Lift(x)) (%y.UU) (%z.f[z])"
     2.9   
    2.10    less_lift_def "less_lift(x1)(x2) == \
    2.11 -\          (case (Rep_Lift(x1))\
    2.12 -\                (% y1.True)\
    2.13 -\                (% y2.case (Rep_Lift(x2))\
    2.14 -\                           (% z1.False)\
    2.15 -\                           (% z2.y2<<z2)))"
    2.16 +\          (sum_case (Rep_Lift(x1))\
    2.17 +\                    (% y1.True)\
    2.18 +\                    (% y2.sum_case (Rep_Lift(x2))\
    2.19 +\                                   (% z1.False)\
    2.20 +\                                   (% z2.y2<<z2)))"
    2.21  
    2.22  end
    2.23  
     3.1 --- a/src/HOLCF/lift1.ML	Mon Jan 24 12:03:53 1994 +0100
     3.2 +++ b/src/HOLCF/lift1.ML	Wed Jan 26 22:07:06 1994 +0100
     3.3 @@ -71,7 +71,7 @@
     3.4   (fn prems =>
     3.5  	[
     3.6  	(rtac (Abs_Lift_inverse RS ssubst) 1),
     3.7 -	(rtac (case_Inl RS ssubst) 1),
     3.8 +	(rtac (sum_case_Inl RS ssubst) 1),
     3.9  	(rtac refl 1)
    3.10  	]);
    3.11  
    3.12 @@ -80,7 +80,7 @@
    3.13   (fn prems =>
    3.14  	[
    3.15  	(rtac (Abs_Lift_inverse RS ssubst) 1),
    3.16 -	(rtac (case_Inr RS ssubst) 1),
    3.17 +	(rtac (sum_case_Inr RS ssubst) 1),
    3.18  	(rtac refl 1)
    3.19  	]);
    3.20  
    3.21 @@ -91,7 +91,7 @@
    3.22   (fn prems =>
    3.23  	[
    3.24  	(rtac (Abs_Lift_inverse RS ssubst) 1),
    3.25 -	(rtac (case_Inl RS ssubst) 1),
    3.26 +	(rtac (sum_case_Inl RS ssubst) 1),
    3.27  	(rtac TrueI 1)
    3.28  	]);
    3.29  
    3.30 @@ -104,8 +104,8 @@
    3.31  	(atac 2),
    3.32  	(rtac (Abs_Lift_inverse RS ssubst) 1),
    3.33  	(rtac (Abs_Lift_inverse RS ssubst) 1),
    3.34 -	(rtac (case_Inr RS ssubst) 1),
    3.35 -	(rtac (case_Inl RS ssubst) 1),
    3.36 +	(rtac (sum_case_Inr RS ssubst) 1),
    3.37 +	(rtac (sum_case_Inl RS ssubst) 1),
    3.38  	(rtac refl 1)
    3.39  	]);
    3.40  
    3.41 @@ -115,8 +115,8 @@
    3.42  	[
    3.43  	(rtac (Abs_Lift_inverse RS ssubst) 1),
    3.44  	(rtac (Abs_Lift_inverse RS ssubst) 1),
    3.45 -	(rtac (case_Inr RS ssubst) 1),
    3.46 -	(rtac (case_Inr RS ssubst) 1),
    3.47 +	(rtac (sum_case_Inr RS ssubst) 1),
    3.48 +	(rtac (sum_case_Inr RS ssubst) 1),
    3.49  	(rtac refl 1)
    3.50  	]);
    3.51  
     4.1 --- a/src/HOLCF/lift1.thy	Mon Jan 24 12:03:53 1994 +0100
     4.2 +++ b/src/HOLCF/lift1.thy	Wed Jan 26 22:07:06 1994 +0100
     4.3 @@ -40,14 +40,14 @@
     4.4    Iup_def       "Iup(x)  == Abs_Lift(Inr(x))"
     4.5  
     4.6    Ilift_def     "Ilift(f)(x)==\
     4.7 -\                case  (Rep_Lift(x)) (%y.UU) (%z.f[z])"
     4.8 +\                sum_case  (Rep_Lift(x)) (%y.UU) (%z.f[z])"
     4.9   
    4.10    less_lift_def "less_lift(x1)(x2) == \
    4.11 -\          (case (Rep_Lift(x1))\
    4.12 -\                (% y1.True)\
    4.13 -\                (% y2.case (Rep_Lift(x2))\
    4.14 -\                           (% z1.False)\
    4.15 -\                           (% z2.y2<<z2)))"
    4.16 +\          (sum_case (Rep_Lift(x1))\
    4.17 +\                    (% y1.True)\
    4.18 +\                    (% y2.sum_case (Rep_Lift(x2))\
    4.19 +\                                   (% z1.False)\
    4.20 +\                                   (% z2.y2<<z2)))"
    4.21  
    4.22  end
    4.23