Replaced some blasts by rules.

--- a/src/HOL/Transitive_Closure.thy	Wed Nov 27 17:06:47 2002 +0100
+++ b/src/HOL/Transitive_Closure.thy	Wed Nov 27 17:07:05 2002 +0100
@@ -199,8 +199,8 @@
   show ?thesis
     apply (subgoal_tac "x = z | (EX y. (x,y) : r & (y,z) : r^*)")
      apply (rule_tac [2] major [THEN converse_rtrancl_induct])
-      prefer 2 apply (blast!)
-     prefer 2 apply (blast!)
+      prefer 2 apply rules
+     prefer 2 apply rules
     apply (erule asm_rl exE disjE conjE prems)+
     done
 qed