# HG changeset patch
# User lcp
# Date 785670465 -3600
# Node ID 281881c083975ea84d0b360e3e513a8ddaa74edb
# Parent  786f32e0b64ef9ed95e78c0682c3dcce69b0e765
added comments on alternative uses of type_intrs/elims

diff -r 786f32e0b64e -r 281881c08397 src/ZF/ex/Term.thy
--- a/src/ZF/ex/Term.thy	Thu Nov 24 10:38:08 1994 +0100
+++ b/src/ZF/ex/Term.thy	Thu Nov 24 10:47:45 1994 +0100
@@ -20,7 +20,11 @@
 datatype
   "term(A)" = Apply ("a: A", "l: list(term(A))")
   monos	      "[list_mono]"
-  type_intrs  "[list_univ RS subsetD]"
+
+  type_elims  "[make_elim (list_univ RS subsetD)]"
+(*Or could have
+    type_intrs  "[list_univ RS subsetD]"
+*)
 
 rules
   term_rec_def