--- a/src/ZF/equalities.ML Wed Dec 14 16:54:13 1994 +0100
+++ b/src/ZF/equalities.ML Wed Dec 14 16:57:55 1994 +0100
@@ -115,6 +115,10 @@
by (fast_tac eq_cs 1);
qed "Diff_0";
+goal ZF.thy "A-B=0 <-> A<=B";
+by (fast_tac (eq_cs addEs [equalityE]) 1);
+qed "Diff_eq_0_iff";
+
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
goal ZF.thy "A - cons(a,B) = A - B - {a}";
by (fast_tac eq_cs 1);
@@ -450,6 +454,11 @@
by (fast_tac eq_cs 1);
qed "converse_diff";
+(*Does the analogue hold for INT?*)
+goal ZF.thy "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))";
+by (fast_tac eq_cs 1);
+qed "converse_UN";
+
(** Pow **)
goal ZF.thy "Pow(A) Un Pow(B) <= Pow(A Un B)";