# HG changeset patch
# User paulson
# Date 1051095996 -7200
# Node ID 17d0e17c8efe212d0e647ece87ec82ea0ec5c238
# Parent  2134ed516b1bb202ada289dc74238871c6937e5e
Got rid of the [iff], which was effectively inserting converseD

diff -r 2134ed516b1b -r 17d0e17c8efe src/ZF/equalities.thy
--- a/src/ZF/equalities.thy	Wed Apr 23 00:14:55 2003 +0200
+++ b/src/ZF/equalities.thy	Wed Apr 23 13:06:36 2003 +0200
@@ -70,10 +70,10 @@
 
 subsection{*Converse of a Relation*}
 
-lemma converse_iff [iff]: "<a,b>: converse(r) <-> <b,a>:r"
+lemma converse_iff [simp]: "<a,b>: converse(r) <-> <b,a>:r"
 by (unfold converse_def, blast)
 
-lemma converseI: "<a,b>:r ==> <b,a>:converse(r)"
+lemma converseI [intro!]: "<a,b>:r ==> <b,a>:converse(r)"
 by (unfold converse_def, blast)
 
 lemma converseD: "<a,b> : converse(r) ==> <b,a> : r"