changeset 13726 | 9550a6f4ed4a |
parent 13704 | 854501b1e957 |
child 13867 | 1fdecd15437f |
--- 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