# HG changeset patch
# User paulson
# Date 1227279293 -3600
# Node ID 111bbd2b12db03849c79fcec06d9ed6b1de749d6
# Parent  381a3b3139ae2f2cfc79cc3153a4577a23d8d55b
Added a line that was missing from the definition

diff -r 381a3b3139ae -r 111bbd2b12db doc-src/ZF/ZF.tex
--- a/doc-src/ZF/ZF.tex	Fri Nov 21 14:21:42 2008 +0100
+++ b/doc-src/ZF/ZF.tex	Fri Nov 21 15:54:53 2008 +0100
@@ -1665,6 +1665,7 @@
 consts     term :: "i=>i"
 datatype  "term(A)" = Apply ("a \isasymin A", "l \isasymin list(term(A))")
   monos list_mono
+  type_elims list_univ [THEN subsetD, elim_format]
 \end{alltt*}
 is an example of nested recursion.  (The theorem \isa{list_mono} is proved
 in theory \isa{List}, and the \isa{term} example is developed in