# HG changeset patch
# User pusch
# Date 857660663 -3600
# Node ID e28a0668dbfe4fcc719c773604dbdd37e9a3d60c
# Parent  a43320c05e843474cf1bc103c99d3e79a077bcc9
primrec definition for nth

diff -r a43320c05e84 -r e28a0668dbfe src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Mar 06 12:32:58 1997 +0100
+++ b/src/HOL/List.thy	Thu Mar 06 16:04:23 1997 +0100
@@ -91,8 +91,9 @@
 primrec take list
   take_Nil  "take n [] = []"
   take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
-defs
-  nth_def  "nth(n) == nat_rec hd (%m r xs. r(tl(xs))) n"
+primrec nth nat
+  "nth 0 xs = hd xs"
+  "nth (Suc n) xs = nth n (tl xs)"
 primrec takeWhile list
   "takeWhile P [] = []"
   "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"