# HG changeset patch
# User nipkow
# Date 865523945 -7200
# Node ID c068bd2f0bbd58f0e850fa3d1bb15fe99e14f0e4
# Parent  804c8a178a7f98c4cbb1491edd2c05d517485422
Moved image_is_empty from Finite.ML to equalities.ML

diff -r 804c8a178a7f -r c068bd2f0bbd src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Thu Jun 05 14:40:35 1997 +0200
+++ b/src/HOL/Finite.ML	Thu Jun 05 17:19:05 1997 +0200
@@ -128,12 +128,6 @@
 qed "finite_Diff_singleton";
 AddIffs [finite_Diff_singleton];
 
-(*** FIXME -> equalities.ML ***)
-goal Set.thy "(f``A = {}) = (A = {})";
-by (blast_tac (!claset addSEs [equalityE]) 1);
-qed "image_is_empty";
-Addsimps [image_is_empty];
-
 goal Finite.thy "!!A. finite B ==> !A. f``A = B --> inj_onto f A --> finite A";
 by (etac finite_induct 1);
  by (ALLGOALS Asm_simp_tac);
diff -r 804c8a178a7f -r c068bd2f0bbd src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Thu Jun 05 14:40:35 1997 +0200
+++ b/src/HOL/equalities.ML	Thu Jun 05 17:19:05 1997 +0200
@@ -111,6 +111,11 @@
 qed "insert_image";
 Addsimps [insert_image];
 
+goal Set.thy "(f``A = {}) = (A = {})";
+by (blast_tac (!claset addSEs [equalityE]) 1);
+qed "image_is_empty";
+AddIffs [image_is_empty];
+
 goalw Set.thy [image_def]
 "(%x. if P x then f x else g x) `` S                    \
 \ = (f `` ({x.x:S & P x})) Un (g `` ({x.x:S & ~(P x)}))";