--- 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"