src/HOL/MicroJava/BV/Semilat.thy

  apply (case_tac "(y,x') : r^*")
   apply blast
  apply (blast elim: converse_rtranclE dest: single_valuedD)
 apply (rule exI)
 apply (rule conjI)
- apply (blast intro: rtrancl_into_rtrancl2 dest: single_valuedD)
-apply (blast intro: rtrancl_into_rtrancl rtrancl_into_rtrancl2 
+ apply (blast intro: converse_rtrancl_into_rtrancl dest: single_valuedD)
+apply (blast intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl 
              elim: converse_rtranclE dest: single_valuedD)
 done
 
 lemma single_valued_has_lubs [rule_format]:
   "[| single_valued r; (x,u) : r^* |] ==> (!y. (y,u) : r^* --> 
   (EX z. is_lub (r^* ) x y z))"
 apply (erule converse_rtrancl_induct)
  apply clarify
  apply (erule converse_rtrancl_induct)
   apply blast
- apply (blast intro: rtrancl_into_rtrancl2)
+ apply (blast intro: converse_rtrancl_into_rtrancl)
 apply (blast intro: extend_lub)
 done
 
 lemma some_lub_conv:
   "[| acyclic r; is_lub (r^* ) x y u |] ==> some_lub (r^* ) x y = u"

  apply simp
 apply(rename_tac x x')
 apply(subgoal_tac "r \<inter> {a. (x,a) \<in> r\<^sup>*} \<times> {b. (b,y) \<in> r\<^sup>*} =
                    insert (x,x') (r \<inter> {a. (x', a) \<in> r\<^sup>*} \<times> {b. (b, y) \<in> r\<^sup>*})")
  apply simp
-apply(blast intro:rtrancl_into_rtrancl2
+apply(blast intro:converse_rtrancl_into_rtrancl
             elim:converse_rtranclE dest:single_valuedD)
 done
 
 
 lemma "\<lbrakk> acyclic r; !x y. (x,y) \<in> r \<longrightarrow> f x = y; is_lub (r\<^sup>*) x y u \<rbrakk> \<Longrightarrow>