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