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.
now uses datatype_intrs and datatype_elims
authorlcp
Thu, 28 Oct 1993 11:30:35 +0100
changeset 84 01d6c0ddaae3
parent 83 de9316670e89
child 85 914270f33f2d
now uses datatype_intrs and datatype_elims
src/ZF/List.ML file | annotate | diff | comparison | revisions
src/ZF/list.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/List.ML	Thu Oct 28 11:28:36 1993 +0100
+++ b/src/ZF/List.ML	Thu Oct 28 11:30:35 1993 +0100
@@ -19,7 +19,7 @@
        "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"];
   val monos = [];
   val type_intrs = datatype_intrs
-  val type_elims = []);
+  val type_elims = datatype_elims);
 
 val [NilI, ConsI] = List.intrs;
 
--- a/src/ZF/list.ML	Thu Oct 28 11:28:36 1993 +0100
+++ b/src/ZF/list.ML	Thu Oct 28 11:30:35 1993 +0100
@@ -19,7 +19,7 @@
        "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"];
   val monos = [];
   val type_intrs = datatype_intrs
-  val type_elims = []);
+  val type_elims = datatype_elims);
 
 val [NilI, ConsI] = List.intrs;
isabelle