# 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< [ (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<