# HG changeset patch
# User paulson
# Date 840709465 -7200
# Node ID 979e8b4f5fa5f63118a6706837c498ea52e0d1cb
# Parent  ec67a0507c2a9febd7f732301515d9155d092461
Proved set_of_list_subset_Cons

diff -r ec67a0507c2a -r 979e8b4f5fa5 src/HOL/List.ML
--- a/src/HOL/List.ML	Thu Aug 22 12:18:21 1996 +0200
+++ b/src/HOL/List.ML	Thu Aug 22 12:24:25 1996 +0200
@@ -94,6 +94,11 @@
 by (Fast_tac 1);
 qed "set_of_list_mem_eq";
 
+goal List.thy "set_of_list l <= set_of_list (x#l)";
+by (Simp_tac 1);
+by (Fast_tac 1);
+qed "set_of_list_subset_Cons";
+
 
 (** list_all **)