# HG changeset patch
# User paulson
# Date 1094200025 -7200
# Node ID e7616269fdca84592c31a8e81b12b6a916b8abc4
# Parent  2fd60846f485b7642b6d9a051a1e684660288771
new theorem symD

diff -r 2fd60846f485 -r e7616269fdca src/HOL/Relation.thy
--- 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"