# HG changeset patch
# User lcp
# Date 793903257 -3600
# Node ID 1f99a44c10cbd5ccc1431c5500acca0115911d05
# Parent  61fcac0e50fc6210e9abe294ecbca346a1ba45fa
Updated comment about list_subset_univ and list_into_univ.

diff -r 61fcac0e50fc -r 1f99a44c10cb src/ZF/List.ML
--- a/src/ZF/List.ML	Mon Feb 27 17:27:50 1995 +0100
+++ b/src/ZF/List.ML	Mon Feb 27 17:40:57 1995 +0100
@@ -46,7 +46,7 @@
 			    Pair_in_univ]) 1);
 qed "list_univ";
 
-(*These two theorems are unused -- useful??*)
+(*These two theorems justify datatypes involving list(nat), list(A), ...*)
 bind_thm ("list_subset_univ", ([list_mono, list_univ] MRS subset_trans));
 
 goal List.thy "!!l A B. [| l: list(A);  A <= univ(B) |] ==> l: univ(B)";