src/HOLCF/lift1.ML
changeset 248 0d0a6a17a02f
parent 243 c22b85994e17
     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