
diff -r e487bf0ed6c4 -r 244daa75f890 src/HOL/List.thy
--- 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
 




