src/HOL/Bali/Basis.thy
changeset 13867 1fdecd15437f
parent 13688 a0b16d42d489
child 14981 e73f8140af78
     1.1 --- a/src/HOL/Bali/Basis.thy	Mon Mar 17 17:37:48 2003 +0100
     1.2 +++ b/src/HOL/Bali/Basis.thy	Mon Mar 17 18:38:50 2003 +0100
     1.3 @@ -62,11 +62,10 @@
     1.4  apply auto
     1.5  done
     1.6  
     1.7 -(* context (theory "Transitive_Closure") *)
     1.8 +(* irrefl_tranclI in Transitive_Closure.thy is more general *)
     1.9  lemma irrefl_tranclI': "r^-1 Int r^+ = {} ==> !x. (x, x) ~: r^+"
    1.10 -apply (rule allI)
    1.11 -apply (erule irrefl_tranclI)
    1.12 -done
    1.13 +by(blast elim: tranclE dest: trancl_into_rtrancl)
    1.14 +
    1.15  
    1.16  lemma trancl_rtrancl_trancl:
    1.17  "\<lbrakk>(x,y)\<in>r^+; (y,z)\<in>r^*\<rbrakk> \<Longrightarrow> (x,z)\<in>r^+"