Mod because of not1_or.
authornipkow
Tue, 10 Mar 1998 20:24:04 +0100
changeset 4726 6b7027b9e3f4
parent 4725 7edba45a6998
child 4727 b820f57a2323
Mod because of not1_or.
src/HOL/Lex/MaxPrefix.ML
--- 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);