# HG changeset patch
# User wenzelm
# Date 899480064 -7200
# Node ID 229190f9f303b5c904ff96791b83563319527974
# Parent  5c1f89ae8aefdb83352db3500dda6546e89a1eb1
removed duplicate thms;

diff -r 5c1f89ae8aef -r 229190f9f303 src/HOL/List.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);
diff -r 5c1f89ae8aef -r 229190f9f303 src/HOL/Vimage.ML
--- 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";