added comments on alternative uses of type_intrs/elims

--- 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