removed duplicate thms;
authorwenzelm
Fri, 03 Jul 1998 17:34:24 +0200
changeset 5122 229190f9f303
parent 5121 5c1f89ae8aef
child 5123 97c1d5c7b701
removed duplicate thms;
src/HOL/List.ML
src/HOL/Vimage.ML
--- 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);
--- a/src/HOL/Vimage.ML	Fri Jul 03 17:33:47 1998 +0200
+++ b/src/HOL/Vimage.ML	Fri Jul 03 17:34:24 1998 +0200
@@ -80,10 +80,6 @@
 by (Blast_tac 1);
 qed "vimage_insert";
 
-Goal "f-``(A Int B) = (f-``A) Int (f-``B)";
-by (Blast_tac 1);
-qed "vimage_Int";
-
 Goal "f-``(A-B) = (f-``A) - (f-``B)";
 by (Blast_tac 1);
 qed "vimage_Diff";