a new theorem from Bryan Ford
authorpaulson
Wed Feb 14 12:16:32 2001 +0100 (2001-02-14)
changeset 11115285b31e9e026
parent 11114 a0c3f2082c88
child 11116 ac51bafd1afb
a new theorem from Bryan Ford
src/HOL/Transitive_Closure.thy
     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