a new theorem from Bryan Ford

--- 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