src/HOL/NanoJava/TypeRel.thy
changeset 13867 1fdecd15437f
parent 12264 9c356e2da72f
child 14134 0fdf5708c7a8
     1.1 --- a/src/HOL/NanoJava/TypeRel.thy	Mon Mar 17 17:37:48 2003 +0100
     1.2 +++ b/src/HOL/NanoJava/TypeRel.thy	Mon Mar 17 18:38:50 2003 +0100
     1.3 @@ -83,11 +83,10 @@
     1.4  lemma subcls1_irrefl_lemma1: "ws_prog \<Longrightarrow> subcls1^-1 \<inter> subcls1^+ = {}"
     1.5  by (fast dest: subcls1D ws_progD)
     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  lemmas subcls1_irrefl_lemma2 = subcls1_irrefl_lemma1 [THEN irrefl_tranclI']
    1.17