# HG changeset patch
# User nipkow
# Date 1021297521 -7200
# Node ID 491a48cf602338c84dfc2e4941ce4b72c692f60c
# Parent  f43153b6336119a319a87836ebd9f053b813140f
*** empty log message ***

diff -r f43153b63361 -r 491a48cf6023 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon May 13 15:39:56 2002 +0200
+++ b/src/HOL/List.thy	Mon May 13 15:45:21 2002 +0200
@@ -1,7 +1,7 @@
-(*Title:HOL/List.thy
-ID: $Id$
-Author: Tobias Nipkow
-Copyright 1994 TU Muenchen
+(* Title:HOL/List.thy
+   ID: $Id$
+   Author: Tobias Nipkow
+   Copyright 1994 TU Muenchen
 *)
 
 header {* The datatype of finite lists *}
@@ -171,7 +171,7 @@
 "remdups [] = []"
 "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
 primrec
-replicate_0: "replicate0x = []"
+replicate_0: "replicate 0 x = []"
 replicate_Suc: "replicate (Suc n) x = x # replicate n x"
 defs
  list_all2_def: