src/HOL/List.ML
changeset 5448 40a09282ba14
parent 5443 e2459d18ff47
child 5518 654ead0ba4f7
     1.1 --- a/src/HOL/List.ML	Wed Sep 09 17:34:58 1998 +0200
     1.2 +++ b/src/HOL/List.ML	Thu Sep 10 17:15:48 1998 +0200
     1.3 @@ -649,16 +649,10 @@
     1.4  by Auto_tac;
     1.5  qed_spec_mp "in_set_butlastD";
     1.6  
     1.7 -Goal "x:set(butlast xs) ==> x:set(butlast(xs@ys))";
     1.8 -by (asm_simp_tac (simpset() addsimps [butlast_append]) 1);
     1.9 -by (blast_tac (claset() addDs [in_set_butlastD]) 1);
    1.10 -qed "in_set_butlast_appendI1";
    1.11 -
    1.12 -Goal "x:set(butlast ys) ==> x:set(butlast(xs@ys))";
    1.13 -by (asm_simp_tac (simpset() addsimps [butlast_append]) 1);
    1.14 -by (Clarify_tac 1);
    1.15 -by (Full_simp_tac 1);
    1.16 -qed "in_set_butlast_appendI2";
    1.17 +Goal "x:set(butlast xs) | x:set(butlast ys) ==> x:set(butlast(xs@ys))";
    1.18 +by (auto_tac (claset() addDs [in_set_butlastD],
    1.19 +	      simpset() addsimps [butlast_append]));
    1.20 +qed "in_set_butlast_appendI";
    1.21  
    1.22  (** take  & drop **)
    1.23  section "take & drop";