src/HOL/List.ML
changeset 7570 a9391550eea1
parent 7246 33058867d6eb
child 8009 29a7a79ee7f4
     1.1 --- a/src/HOL/List.ML	Tue Sep 21 19:10:39 1999 +0200
     1.2 +++ b/src/HOL/List.ML	Tue Sep 21 19:11:07 1999 +0200
     1.3 @@ -804,6 +804,7 @@
     1.4  by (exhaust_tac "na" 1);
     1.5   by Auto_tac;
     1.6  qed_spec_mp "take_take";
     1.7 +Addsimps [take_take];
     1.8  
     1.9  Goal "!xs. drop n (drop m xs) = drop (n + m) xs"; 
    1.10  by (induct_tac "m" 1);
    1.11 @@ -811,6 +812,7 @@
    1.12  by (exhaust_tac "xs" 1);
    1.13   by Auto_tac;
    1.14  qed_spec_mp "drop_drop";
    1.15 +Addsimps [drop_drop];
    1.16  
    1.17  Goal "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; 
    1.18  by (induct_tac "m" 1);