new theorem symD
authorpaulson
Fri Sep 03 10:27:05 2004 +0200 (2004-09-03)
changeset 15177e7616269fdca
parent 15176 2fd60846f485
child 15178 5f621aa35c25
new theorem symD
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Relation.thy	Fri Sep 03 10:26:39 2004 +0200
     1.2 +++ b/src/HOL/Relation.thy	Fri Sep 03 10:27:05 2004 +0200
     1.3 @@ -162,7 +162,10 @@
     1.4    by (unfold antisym_def) rules
     1.5  
     1.6  
     1.7 -subsection {* Transitivity *}
     1.8 +subsection {* Symmetry and Transitivity *}
     1.9 +
    1.10 +lemma symD: "sym r ==> (a, b) : r ==> (b, a) : r"
    1.11 +  by (unfold sym_def, blast)
    1.12  
    1.13  lemma transI:
    1.14    "(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r"