# HG changeset patch
# User paulson
# Date 905440548 -7200
# Node ID 40a09282ba14252269c1d6464708824d4e0120f4
# Parent  df03d330aeabc337a1d9b262389be67e035562de
in_set_butlast_appendI supersedes in_set_butlast_appendI1,2

diff -r df03d330aeab -r 40a09282ba14 src/HOL/List.ML
--- a/src/HOL/List.ML	Wed Sep 09 17:34:58 1998 +0200
+++ b/src/HOL/List.ML	Thu Sep 10 17:15:48 1998 +0200
@@ -649,16 +649,10 @@
 by Auto_tac;
 qed_spec_mp "in_set_butlastD";
 
-Goal "x:set(butlast xs) ==> x:set(butlast(xs@ys))";
-by (asm_simp_tac (simpset() addsimps [butlast_append]) 1);
-by (blast_tac (claset() addDs [in_set_butlastD]) 1);
-qed "in_set_butlast_appendI1";
-
-Goal "x:set(butlast ys) ==> x:set(butlast(xs@ys))";
-by (asm_simp_tac (simpset() addsimps [butlast_append]) 1);
-by (Clarify_tac 1);
-by (Full_simp_tac 1);
-qed "in_set_butlast_appendI2";
+Goal "x:set(butlast xs) | x:set(butlast ys) ==> x:set(butlast(xs@ys))";
+by (auto_tac (claset() addDs [in_set_butlastD],
+	      simpset() addsimps [butlast_append]));
+qed "in_set_butlast_appendI";
 
 (** take  & drop **)
 section "take & drop";