# HG changeset patch
# User paulson
# Date 951731348 -3600
# Node ID cc2340c338f0cc3d42c5782ae0e1635689567c20
# Parent  a054d5c98b21be3b64a04ce2086c99a2f3c15b72
new thm vimage_Collect_eq

diff -r a054d5c98b21 -r cc2340c338f0 src/HOL/Vimage.ML
--- a/src/HOL/Vimage.ML	Mon Feb 28 10:48:39 2000 +0100
+++ b/src/HOL/Vimage.ML	Mon Feb 28 10:49:08 2000 +0100
@@ -71,9 +71,17 @@
 by (Blast_tac 1);
 qed "vimage_INT";
 
-bind_thm ("vimage_Collect", allI RS prove_goalw thy [vimage_def]
-  "! x. P (f x) = Q x ==> f -`` (Collect P) = Collect Q"
-    (fn prems => [cut_facts_tac prems 1, Fast_tac 1]));
+Goal "f -`` Collect P = {y. P (f y)}";
+by (Blast_tac 1);
+qed "vimage_Collect_eq";
+Addsimps [vimage_Collect_eq];
+
+(*A strange result used in Tools/inductive_package*)
+bind_thm ("vimage_Collect", 
+	  allI RS 
+	  prove_goalw thy [vimage_def]
+	  "! x. P (f x) = Q x ==> f -`` (Collect P) = Collect Q"
+	      (fn prems => [cut_facts_tac prems 1, Fast_tac 1]));
 
 Addsimps [vimage_empty, vimage_Un, vimage_Int];