--- 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";