| changeset 1936 | 979e8b4f5fa5 |
| parent 1908 | 55d8e38262a8 |
| child 1985 | 84cf16192e03 |
--- 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 **)