moved identity theorems to Fun.ML

--- a/src/HOL/Vimage.ML	Wed Sep 08 15:38:54 1999 +0200
+++ b/src/HOL/Vimage.ML	Wed Sep 08 15:39:52 1999 +0200
@@ -43,11 +43,6 @@
 
 (*** Simple equalities ***)
 
-Goal "(%x. x) -`` B = B";
-by (Blast_tac 1);
-qed "ident_vimage";
-Addsimps [ident_vimage];
-
 Goal "f-``{} = {}";
 by (Blast_tac 1);
 qed "vimage_empty";

--- a/src/HOL/equalities.ML	Wed Sep 08 15:38:54 1999 +0200
+++ b/src/HOL/equalities.ML	Wed Sep 08 15:39:52 1999 +0200
@@ -101,11 +101,6 @@
 qed "image_insert";
 Addsimps[image_insert];
 
-Goal "(%x. x) `` Y = Y";
-by (Blast_tac 1);
-qed "image_id";
-Addsimps [image_id];
-
 Goal "x:A ==> (%x. c) `` A = {c}";
 by (Blast_tac 1);
 qed "image_constant";
@@ -619,6 +614,11 @@
 by (Blast_tac 1);
 qed "Diff_eq";
 
+Goal "(A-B = {}) = (A<=B)";
+by (Blast_tac 1);
+qed "Diff_eq_empty_iff";
+Addsimps[Diff_eq_empty_iff];
+
 Goal "A-A = {}";
 by (Blast_tac 1);
 qed "Diff_cancel";