| changeset 5122 | 229190f9f303 |
| parent 5077 | 71043526295f |
| child 5129 | 99ffd3dfb180 |
--- a/src/HOL/List.ML Fri Jul 03 17:33:47 1998 +0200 +++ b/src/HOL/List.ML Fri Jul 03 17:34:24 1998 +0200 @@ -381,12 +381,6 @@ qed "set_map"; Addsimps [set_map]; -Goal "set(map f xs) = f``(set xs)"; -by (induct_tac "xs" 1); -by (ALLGOALS Asm_simp_tac); -qed "set_map"; -Addsimps [set_map]; - Goal "(x : set(filter P xs)) = (x : set xs & P x)"; by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac);