new theorem symD

--- a/src/HOL/Relation.thy	Fri Sep 03 10:26:39 2004 +0200
+++ b/src/HOL/Relation.thy	Fri Sep 03 10:27:05 2004 +0200
@@ -162,7 +162,10 @@
   by (unfold antisym_def) rules
 
 
-subsection {* Transitivity *}
+subsection {* Symmetry and Transitivity *}
+
+lemma symD: "sym r ==> (a, b) : r ==> (b, a) : r"
+  by (unfold sym_def, blast)
 
 lemma transI:
   "(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r"