# HG changeset patch
# User paulson
# Date 959260460 -7200
# Node ID b734bdb6042da3b28dff040176ae4b38aa788d38
# Parent  881853835a37084d9bcad57555025b03f2c48ff1
better indentation; declared function "null"

diff -r 881853835a37 -r b734bdb6042d src/HOL/List.thy
--- a/src/HOL/List.thy	Thu May 25 15:13:57 2000 +0200
+++ b/src/HOL/List.thy	Thu May 25 15:14:20 2000 +0200
@@ -32,7 +32,7 @@
   zip	      :: "'a list => 'b list => ('a * 'b) list"
   upt         :: nat => nat => nat list                   ("(1[_../_'(])")
   remdups     :: 'a list => 'a list
-  nodups      :: "'a list => bool"
+  null, nodups :: "'a list => bool"
   replicate   :: nat => 'a => 'a list
 
 nonterminals
@@ -85,15 +85,18 @@
 primrec
   "hd(x#xs) = x"
 primrec
-  "tl([]) = []"
+  "tl([])   = []"
   "tl(x#xs) = xs"
 primrec
+  "null([])   = True"
+  "null(x#xs) = False"
+primrec
   "last(x#xs) = (if xs=[] then x else last xs)"
 primrec
-  "butlast [] = []"
+  "butlast []    = []"
   "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
 primrec
-  "x mem [] = False"
+  "x mem []     = False"
   "x mem (y#ys) = (if y=x then True else x mem ys)"
 primrec
   "set [] = {}"
@@ -102,25 +105,25 @@
   list_all_Nil  "list_all P [] = True"
   list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
 primrec
-  "map f [] = []"
+  "map f []     = []"
   "map f (x#xs) = f(x)#map f xs"
 primrec
   append_Nil  "[]    @ys = ys"
   append_Cons "(x#xs)@ys = x#(xs@ys)"
 primrec
-  "rev([]) = []"
+  "rev([])   = []"
   "rev(x#xs) = rev(xs) @ [x]"
 primrec
-  "filter P [] = []"
+  "filter P []     = []"
   "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
 primrec
   foldl_Nil  "foldl f a [] = a"
   foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"
 primrec
-  "foldr f [] a = a"
+  "foldr f [] a     = a"
   "foldr f (x#xs) a = f x (foldr f xs a)"
 primrec
-  "concat([]) = []"
+  "concat([])   = []"
   "concat(x#xs) = x @ concat(xs)"
 primrec
   drop_Nil  "drop n [] = []"
@@ -141,10 +144,10 @@
  "(x#xs)[i:=v] = (case i of 0     => v # xs 
 			  | Suc j => x # xs[j:=v])"
 primrec
-  "takeWhile P [] = []"
+  "takeWhile P []     = []"
   "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
 primrec
-  "dropWhile P [] = []"
+  "dropWhile P []     = []"
   "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
 primrec
   "zip xs []     = []"