# HG changeset patch
# User paulson
# Date 982149392 -3600
# Node ID 285b31e9e02602f3daf43e04eb7d93163046bb56
# Parent  a0c3f2082c88b51a1c4174d4be849ac50d0de3ff
a new theorem from Bryan Ford

diff -r a0c3f2082c88 -r 285b31e9e026 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Wed Feb 14 11:18:39 2001 +0100
+++ b/src/HOL/Transitive_Closure.thy	Wed Feb 14 12:16:32 2001 +0100
@@ -85,4 +85,9 @@
 lemma trancl_range [simp]: "Range (r^+) = Range r"
   by (simp add: Range_def trancl_converse [symmetric])
 
+lemma Not_Domain_rtrancl:
+	"x ~: Domain R ==> ((x, y) : R^*) = (x = y)"
+ apply (auto)
+ by (erule rev_mp, erule rtrancl_induct, auto)
+ 
 end