changeset 8423 | 3c19160b6432 |
parent 8064 | 357652a08ee0 |
child 8442 | 96023903c2df |
--- a/src/HOL/IMP/Transition.ML Mon Mar 13 12:42:41 2000 +0100 +++ b/src/HOL/IMP/Transition.ML Mon Mar 13 12:51:10 2000 +0100 @@ -220,7 +220,7 @@ by (Clarify_tac 1); by (etac rel_pow_E2 1); by (asm_full_simp_tac (simpset() addsimps evalc.intrs) 1); -by (exhaust_tac "c" 1); +by (cases_tac "c" 1); by (fast_tac (claset() addSDs [hlemma]) 1); by (Blast_tac 1); by (blast_tac (claset() addSDs [rel_pow_Suc_I2 RS comp_decomp_lemma]) 1);