Added take_all and drop_all to simpset.
authornipkow
Wed Aug 18 10:27:57 1999 +0200 (1999-08-18)
changeset 724633058867d6eb
parent 7245 65ccac4e1f3f
child 7247 aad87acc8fa3
Added take_all and drop_all to simpset.
src/HOL/List.ML
     1.1 --- a/src/HOL/List.ML	Tue Aug 17 22:24:15 1999 +0200
     1.2 +++ b/src/HOL/List.ML	Wed Aug 18 10:27:57 1999 +0200
     1.3 @@ -770,6 +770,7 @@
     1.4  by (exhaust_tac "xs" 1);
     1.5   by Auto_tac;
     1.6  qed_spec_mp "take_all";
     1.7 +Addsimps [take_all];
     1.8  
     1.9  Goal "!xs. length xs <= n --> drop n xs = []";
    1.10  by (induct_tac "n" 1);
    1.11 @@ -777,6 +778,7 @@
    1.12  by (exhaust_tac "xs" 1);
    1.13   by Auto_tac;
    1.14  qed_spec_mp "drop_all";
    1.15 +Addsimps [drop_all];
    1.16  
    1.17  Goal "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
    1.18  by (induct_tac "n" 1);