1.1 --- a/src/HOL/List.thy	Thu May 25 15:13:57 2000 +0200
     1.2 +++ b/src/HOL/List.thy	Thu May 25 15:14:20 2000 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4    zip	      :: "'a list => 'b list => ('a * 'b) list"
     1.5    upt         :: nat => nat => nat list                   ("(1[_../_'(])")
     1.6    remdups     :: 'a list => 'a list
     1.7 -  nodups      :: "'a list => bool"
     1.8 +  null, nodups :: "'a list => bool"
     1.9    replicate   :: nat => 'a => 'a list
    1.10  
    1.11  nonterminals
    1.12 @@ -85,15 +85,18 @@
    1.13  primrec
    1.14    "hd(x#xs) = x"
    1.15  primrec
    1.16 -  "tl([]) = []"
    1.17 +  "tl([])   = []"
    1.18    "tl(x#xs) = xs"
    1.19  primrec
    1.20 +  "null([])   = True"
    1.21 +  "null(x#xs) = False"
    1.22 +primrec
    1.23    "last(x#xs) = (if xs=[] then x else last xs)"
    1.24  primrec
    1.25 -  "butlast [] = []"
    1.26 +  "butlast []    = []"
    1.27    "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
    1.28  primrec
    1.29 -  "x mem [] = False"
    1.30 +  "x mem []     = False"
    1.31    "x mem (y#ys) = (if y=x then True else x mem ys)"
    1.32  primrec
    1.33    "set [] = {}"
    1.34 @@ -102,25 +105,25 @@
    1.35    list_all_Nil  "list_all P [] = True"
    1.36    list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
    1.37  primrec
    1.38 -  "map f [] = []"
    1.39 +  "map f []     = []"
    1.40    "map f (x#xs) = f(x)#map f xs"
    1.41  primrec
    1.42    append_Nil  "[]    @ys = ys"
    1.43    append_Cons "(x#xs)@ys = x#(xs@ys)"
    1.44  primrec
    1.45 -  "rev([]) = []"
    1.46 +  "rev([])   = []"
    1.47    "rev(x#xs) = rev(xs) @ [x]"
    1.48  primrec
    1.49 -  "filter P [] = []"
    1.50 +  "filter P []     = []"
    1.51    "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
    1.52  primrec
    1.53    foldl_Nil  "foldl f a [] = a"
    1.54    foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"
    1.55  primrec
    1.56 -  "foldr f [] a = a"
    1.57 +  "foldr f [] a     = a"
    1.58    "foldr f (x#xs) a = f x (foldr f xs a)"
    1.59  primrec
    1.60 -  "concat([]) = []"
    1.61 +  "concat([])   = []"
    1.62    "concat(x#xs) = x @ concat(xs)"
    1.63  primrec
    1.64    drop_Nil  "drop n [] = []"
    1.65 @@ -141,10 +144,10 @@
    1.66   "(x#xs)[i:=v] = (case i of 0     => v # xs 
    1.67  			  | Suc j => x # xs[j:=v])"
    1.68  primrec
    1.69 -  "takeWhile P [] = []"
    1.70 +  "takeWhile P []     = []"
    1.71    "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
    1.72  primrec
    1.73 -  "dropWhile P [] = []"
    1.74 +  "dropWhile P []     = []"
    1.75    "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
    1.76  primrec
    1.77    "zip xs []     = []"