Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
sum_case_Inl and sum_case_Inr are now defined in Datatype.ML.
authorberghofe
Thu, 19 Aug 1999 19:01:57 +0200
changeset 7294 5a50de9141b5
parent 7293 959e060f4a2f
child 7295 fe09a0c5cebe
sum_case_Inl and sum_case_Inr are now defined in Datatype.ML.
src/HOLCF/Up1.ML file | annotate | diff | comparison | revisions 
--- 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 =>
         [
isabelle