Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proved set_of_list_subset_Cons
authorpaulson
Thu, 22 Aug 1996 12:24:25 +0200
changeset 1936 979e8b4f5fa5
parent 1935 ec67a0507c2a
child 1937 e59ff0eb1e91
Proved set_of_list_subset_Cons
src/HOL/List.ML file | annotate | diff | comparison | revisions 
--- 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 **)
isabelle