removal of image_Collect as a default simprule

--- a/src/HOL/Lattice/Bounds.thy	Tue Apr 24 12:19:01 2001 +0200
+++ b/src/HOL/Lattice/Bounds.thy	Tue Apr 24 12:19:58 2001 +0200
@@ -315,7 +315,7 @@
   hence "is_Inf (dual ` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b}) (dual inf)"
     by (simp only: dual_Inf dual_leq)
   also have "dual ` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b} = {b'. \<forall>a' \<in> dual ` A. a' \<sqsubseteq> b'}"
-    by (auto iff: dual_ball dual_Collect)  (* FIXME !? *)
+    by (auto iff: dual_ball dual_Collect simp add: image_Collect)  (* FIXME !? *)
   finally have "is_Inf \<dots> (dual inf)" .
   hence "is_Sup (dual ` A) (dual inf)"
     by (rule Inf_Sup)

--- a/src/HOL/List.ML	Tue Apr 24 12:19:01 2001 +0200
+++ b/src/HOL/List.ML	Tue Apr 24 12:19:58 2001 +0200
@@ -1374,6 +1374,7 @@
 qed "wf_lex";
 AddSIs [wf_lex];
 
+
 Goal
  "lexn r n = \
 \ {(xs,ys). length xs = n & length ys = n & \
@@ -1381,15 +1382,14 @@
 by (induct_tac "n" 1);
  by (Simp_tac 1);
  by (Blast_tac 1);
-by (asm_full_simp_tac (simpset() 
-				addsimps [lex_prod_def]) 1);
-by (auto_tac (claset(), simpset()));
+by (asm_full_simp_tac (simpset() addsimps [image_Collect, lex_prod_def]) 1);
+by Auto_tac;
   by (Blast_tac 1);
  by (rename_tac "a xys x xs' y ys'" 1);
  by (res_inst_tac [("x","a#xys")] exI 1);
  by (Simp_tac 1);
 by (case_tac "xys" 1);
- by (ALLGOALS (asm_full_simp_tac (simpset())));
+ by (ALLGOALS Asm_full_simp_tac);
 by (Blast_tac 1);
 qed "lexn_conv";
 

--- a/src/HOL/equalities.ML	Tue Apr 24 12:19:01 2001 +0200
+++ b/src/HOL/equalities.ML	Tue Apr 24 12:19:58 2001 +0200
@@ -142,10 +142,12 @@
 qed "image_is_empty";
 AddIffs [image_is_empty];
 
+(*NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
+  with its implicit quantifier and conjunction.  Also image enjoys better
+  equational properties than does the RHS.*)
 Goal "f ` {x. P x} = {f x | x. P x}";
 by (Blast_tac 1);
 qed "image_Collect";
-Addsimps [image_Collect];
 
 Goalw [image_def] "(%x. if P x then f x else g x) ` S   \
 \                = (f ` (S Int {x. P x})) Un (g ` (S Int {x. ~(P x)}))";