--- a/src/HOL/List.thy Tue Aug 05 16:14:23 1997 +0200
+++ b/src/HOL/List.thy Tue Aug 05 16:21:45 1997 +0200
@@ -26,6 +26,7 @@
dropWhile :: ('a => bool) => 'a list => 'a list
tl,ttl :: 'a list => 'a list
rev :: 'a list => 'a list
+ replicate :: nat => 'a => 'a list
syntax
(* list Enumeration *)
@@ -109,6 +110,9 @@
primrec dropWhile list
"dropWhile P [] = []"
"dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
+primrec replicate nat
+replicate_0 "replicate 0 x = []"
+replicate_Suc "replicate (Suc n) x = x # replicate n x"
end