# HG changeset patch
# User berghofe
# Date 1038413225 -3600
# Node ID 9550a6f4ed4a00f7fd421c59b42b71144e19244b
# Parent  12404b452034b17871fd4b0683ebf454903d77c9
Replaced some blasts by rules.

diff -r 12404b452034 -r 9550a6f4ed4a src/HOL/Transitive_Closure.thy
--- 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