List.thy

--- a/List.thy	Wed Dec 14 11:17:18 1994 +0100
+++ b/List.thy	Thu Jan 26 10:41:21 1995 +0100
@@ -23,6 +23,7 @@
   filter    :: "['a => bool, 'a list] => 'a list"
   foldl     :: "[['b,'a] => 'b, 'b, 'a list] => 'b"
   length    :: "'a list => nat"
+  nth       :: "[nat, 'a list] => 'a"
 
 syntax
   (* list Enumeration *)
@@ -73,4 +74,6 @@
 primrec length list
   length_Nil  "length([]) = 0"
   length_Cons "length(x#xs) = Suc(length(xs))"
+defs
+  nth_def "nth(n) == nat_rec(n, hd, %m r xs. r(tl(xs)))"
 end