diff -r 9df4b3934487 -r fe20540bcf93 src/HOL/MicroJava/BV/Semilat.thy
--- a/src/HOL/MicroJava/BV/Semilat.thy	Thu Dec 20 17:08:55 2001 +0100
+++ b/src/HOL/MicroJava/BV/Semilat.thy	Thu Dec 20 18:22:44 2001 +0100
@@ -198,8 +198,8 @@
  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
 
@@ -210,7 +210,7 @@
  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
 
@@ -246,7 +246,7 @@
 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