patched sum_case;
authorwenzelm
Fri, 30 Apr 1999 16:41:10 +0200
changeset 6543 da7b170fc8a7
parent 6542 015c3813277a
child 6544 22b91f7c30d2
patched sum_case;
src/HOLCF/Up1.ML
src/HOLCF/Up1.thy
--- a/src/HOLCF/Up1.ML	Thu Apr 29 22:45:19 1999 +0200
+++ b/src/HOLCF/Up1.ML	Fri Apr 30 16:41:10 1999 +0200
@@ -6,6 +6,9 @@
 
 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 =>
         [
--- a/src/HOLCF/Up1.thy	Thu Apr 29 22:45:19 1999 +0200
+++ b/src/HOLCF/Up1.thy	Fri Apr 30 16:41:10 1999 +0200
@@ -8,7 +8,7 @@
 
 *)
 
-Up1 = Cfun3 + Sum + 
+Up1 = Cfun3 + Sum + Datatype +
 
 (* new type for lifting *)