# HG changeset patch
# User paulson
# Date 929003849 -7200
# Node ID d5dfe040c183de04960faedde22c2752f5e95bfc
# Parent  6737af18317e4c6f777d20cf9e23e5221bf3a392
tidied

diff -r 6737af18317e -r d5dfe040c183 src/HOL/Lex/Prefix.ML
--- a/src/HOL/Lex/Prefix.ML	Thu Jun 10 10:36:41 1999 +0200
+++ b/src/HOL/Lex/Prefix.ML	Thu Jun 10 10:37:29 1999 +0200
@@ -49,10 +49,7 @@
  by (hyp_subst_tac 1);
  by (asm_full_simp_tac (simpset() delsimps [append_assoc]
                                  addsimps [append_assoc RS sym])1);
-by (etac disjE 1);
- by (Asm_simp_tac 1);
-by (Clarify_tac 1);
-by (Simp_tac 1);
+by (Force_tac 1);
 qed "prefix_snoc";
 Addsimps [prefix_snoc];
 
@@ -85,8 +82,7 @@
 
 Goal "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))";
 by (res_inst_tac [("xs","zs")] rev_induct 1);
- by (Simp_tac 1);
- by (Blast_tac 1);
+ by (Force_tac 1);
 by (asm_full_simp_tac (simpset() delsimps [append_assoc]
                                  addsimps [append_assoc RS sym])1);
 by (Simp_tac 1);