author | nipkow |
Tue, 10 Mar 1998 20:24:04 +0100 | |
changeset 4726 | 6b7027b9e3f4 |
parent 4725 | 7edba45a6998 |
child 4727 | b820f57a2323 |
--- a/src/HOL/Lex/MaxPrefix.ML Tue Mar 10 19:15:00 1998 +0100 +++ b/src/HOL/Lex/MaxPrefix.ML Tue Mar 10 20:24:04 1998 +0100 @@ -41,9 +41,8 @@ be disjE 1; by(Clarify_tac 1); by(Asm_full_simp_tac 1); - by(Blast_tac 1); + by(Blast_tac 1); by(Asm_full_simp_tac 1); - by(Blast_tac 1); by(subgoal_tac "~P(ps)" 1); by(Asm_simp_tac 1); by(fast_tac (claset() addss simpset()) 1);