ZF/domrange/converse_iff: new

--- a/src/ZF/domrange.ML	Thu Nov 03 12:06:37 1994 +0100
+++ b/src/ZF/domrange.ML	Thu Nov 03 12:23:19 1994 +0100
@@ -8,6 +8,10 @@
 
 (*** converse ***)
 
+val converse_iff = prove_goalw ZF.thy [converse_def]
+    "<a,b>: converse(r) <-> <b,a>:r"
+ (fn _ => [ (fast_tac pair_cs 1) ]);
+
 val converseI = prove_goalw ZF.thy [converse_def]
     "!!a b r. <a,b>:r ==> <b,a>:converse(r)"
  (fn _ => [ (fast_tac pair_cs 1) ]);