src/HOL/List.thy
changeset 13147 491a48cf6023
parent 13146 f43153b63361
child 13187 e5434b822a96
     1.1 --- a/src/HOL/List.thy	Mon May 13 15:39:56 2002 +0200
     1.2 +++ b/src/HOL/List.thy	Mon May 13 15:45:21 2002 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4 -(*Title:HOL/List.thy
     1.5 -ID: $Id$
     1.6 -Author: Tobias Nipkow
     1.7 -Copyright 1994 TU Muenchen
     1.8 +(* Title:HOL/List.thy
     1.9 +   ID: $Id$
    1.10 +   Author: Tobias Nipkow
    1.11 +   Copyright 1994 TU Muenchen
    1.12  *)
    1.13  
    1.14  header {* The datatype of finite lists *}
    1.15 @@ -171,7 +171,7 @@
    1.16  "remdups [] = []"
    1.17  "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
    1.18  primrec
    1.19 -replicate_0: "replicate0x = []"
    1.20 +replicate_0: "replicate 0 x = []"
    1.21  replicate_Suc: "replicate (Suc n) x = x # replicate n x"
    1.22  defs
    1.23   list_all2_def: