src/HOL/Transitive_Closure.thy
changeset 25295 12985023be5e
parent 23743 52fbc991039f
child 25425 9191942c4ead
     1.1 --- a/src/HOL/Transitive_Closure.thy	Mon Nov 05 22:00:21 2007 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Nov 05 22:48:37 2007 +0100
     1.3 @@ -449,6 +449,10 @@
     1.4  
     1.5  lemmas tranclD = tranclpD [to_set]
     1.6  
     1.7 +lemma tranclD2:
     1.8 +  "(x, y) \<in> R\<^sup>+ \<Longrightarrow> \<exists>z. (x, z) \<in> R\<^sup>* \<and> (z, y) \<in> R"
     1.9 +  by (blast elim: tranclE intro: trancl_into_rtrancl)
    1.10 +
    1.11  lemma irrefl_tranclI: "r^-1 \<inter> r^* = {} ==> (x, x) \<notin> r^+"
    1.12    by (blast elim: tranclE dest: trancl_into_rtrancl)
    1.13