# HG changeset patch
# User lcp
# Date 783861799 -3600
# Node ID 91bc4b9eee1d58fb8324b2850e0010ee140f6311
# Parent  be908d8d41ef3b4006a87396cb05738131eaee7d
ZF/domrange/converse_iff: new

diff -r be908d8d41ef -r 91bc4b9eee1d src/ZF/domrange.ML
--- 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) ]);