src/HOL/Transitive_Closure.thy
changeset 13726 9550a6f4ed4a
parent 13704 854501b1e957
child 13867 1fdecd15437f
     1.1 --- a/src/HOL/Transitive_Closure.thy	Wed Nov 27 17:06:47 2002 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Nov 27 17:07:05 2002 +0100
     1.3 @@ -199,8 +199,8 @@
     1.4    show ?thesis
     1.5      apply (subgoal_tac "x = z | (EX y. (x,y) : r & (y,z) : r^*)")
     1.6       apply (rule_tac [2] major [THEN converse_rtrancl_induct])
     1.7 -      prefer 2 apply (blast!)
     1.8 -     prefer 2 apply (blast!)
     1.9 +      prefer 2 apply rules
    1.10 +     prefer 2 apply rules
    1.11      apply (erule asm_rl exE disjE conjE prems)+
    1.12      done
    1.13  qed