src/HOL/List.ML
changeset 5122 229190f9f303
parent 5077 71043526295f
child 5129 99ffd3dfb180
     1.1 --- a/src/HOL/List.ML	Fri Jul 03 17:33:47 1998 +0200
     1.2 +++ b/src/HOL/List.ML	Fri Jul 03 17:34:24 1998 +0200
     1.3 @@ -381,12 +381,6 @@
     1.4  qed "set_map";
     1.5  Addsimps [set_map];
     1.6  
     1.7 -Goal "set(map f xs) = f``(set xs)";
     1.8 -by (induct_tac "xs" 1);
     1.9 -by (ALLGOALS Asm_simp_tac);
    1.10 -qed "set_map";
    1.11 -Addsimps [set_map];
    1.12 -
    1.13  Goal "(x : set(filter P xs)) = (x : set xs & P x)";
    1.14  by (induct_tac "xs" 1);
    1.15  by (ALLGOALS Asm_simp_tac);