src/HOL/Transitive_Closure.thy
changeset 11115 285b31e9e026
parent 11090 3041d0347d26
child 11327 cd2c27a23df1
     1.1 --- a/src/HOL/Transitive_Closure.thy	Wed Feb 14 11:18:39 2001 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Feb 14 12:16:32 2001 +0100
     1.3 @@ -85,4 +85,9 @@
     1.4  lemma trancl_range [simp]: "Range (r^+) = Range r"
     1.5    by (simp add: Range_def trancl_converse [symmetric])
     1.6  
     1.7 +lemma Not_Domain_rtrancl:
     1.8 +	"x ~: Domain R ==> ((x, y) : R^*) = (x = y)"
     1.9 + apply (auto)
    1.10 + by (erule rev_mp, erule rtrancl_induct, auto)
    1.11 + 
    1.12  end