Added take_all and drop_all to simpset.
authornipkow
Wed, 18 Aug 1999 10:27:57 +0200
changeset 7246 33058867d6eb
parent 7245 65ccac4e1f3f
child 7247 aad87acc8fa3
Added take_all and drop_all to simpset.
src/HOL/List.ML
--- a/src/HOL/List.ML	Tue Aug 17 22:24:15 1999 +0200
+++ b/src/HOL/List.ML	Wed Aug 18 10:27:57 1999 +0200
@@ -770,6 +770,7 @@
 by (exhaust_tac "xs" 1);
  by Auto_tac;
 qed_spec_mp "take_all";
+Addsimps [take_all];
 
 Goal "!xs. length xs <= n --> drop n xs = []";
 by (induct_tac "n" 1);
@@ -777,6 +778,7 @@
 by (exhaust_tac "xs" 1);
  by Auto_tac;
 qed_spec_mp "drop_all";
+Addsimps [drop_all];
 
 Goal "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
 by (induct_tac "n" 1);