removed duplicate thms;
authorwenzelm
Fri Jul 03 17:34:24 1998 +0200 (1998-07-03)
changeset 5122229190f9f303
parent 5121 5c1f89ae8aef
child 5123 97c1d5c7b701
removed duplicate thms;
src/HOL/List.ML
src/HOL/Vimage.ML
     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);
     2.1 --- a/src/HOL/Vimage.ML	Fri Jul 03 17:33:47 1998 +0200
     2.2 +++ b/src/HOL/Vimage.ML	Fri Jul 03 17:34:24 1998 +0200
     2.3 @@ -80,10 +80,6 @@
     2.4  by (Blast_tac 1);
     2.5  qed "vimage_insert";
     2.6  
     2.7 -Goal "f-``(A Int B) = (f-``A) Int (f-``B)";
     2.8 -by (Blast_tac 1);
     2.9 -qed "vimage_Int";
    2.10 -
    2.11  Goal "f-``(A-B) = (f-``A) - (f-``B)";
    2.12  by (Blast_tac 1);
    2.13  qed "vimage_Diff";