src/HOL/MicroJava/BV/Semilat.thy

--- a/src/HOL/MicroJava/BV/Semilat.thy	Wed Feb 21 15:21:15 2001 +0100
+++ b/src/HOL/MicroJava/BV/Semilat.thy	Thu Feb 22 10:18:41 2001 +0100
@@ -195,8 +195,7 @@
 apply (case_tac "(y,x) : r^*")
  apply (case_tac "(y,x') : r^*")
   apply blast
- apply (blast intro: r_into_rtrancl elim: converse_rtranclE
-               dest: single_valuedD)
+ apply (blast elim: converse_rtranclE dest: single_valuedD)
 apply (rule exI)
 apply (rule conjI)
  apply (blast intro: rtrancl_into_rtrancl2 dest: single_valuedD)