# HG changeset patch # User berghofe # Date 935082117 -7200 # Node ID 5a50de9141b5e2947a3f3f169f8acde63e371b68 # Parent 959e060f4a2fcdfdb269ef93b9fa16a0d5e6aa62 sum_case_Inl and sum_case_Inr are now defined in Datatype.ML. diff -r 959e060f4a2f -r 5a50de9141b5 src/HOLCF/Up1.ML --- a/src/HOLCF/Up1.ML Thu Aug 19 19:00:42 1999 +0200 +++ b/src/HOLCF/Up1.ML Thu Aug 19 19:01:57 1999 +0200 @@ -6,9 +6,6 @@ open Up1; -(*compatibility*) -val [sum_case_Inl, sum_case_Inr] = sum.cases; - qed_goal "Abs_Up_inverse2" thy "Rep_Up (Abs_Up y) = y" (fn prems => [