src/HOL/Relation.thy
changeset 15177 e7616269fdca
parent 15140 322485b816ac
child 17589 58eeffd73be1
     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"