src/HOL/List.thy
changeset 1824 44254696843a
parent 1812 debfc40b7756
child 1898 260a9711f507
--- a/src/HOL/List.thy	Fri Jun 21 13:51:09 1996 +0200
+++ b/src/HOL/List.thy	Tue Jun 25 13:11:29 1996 +0200
@@ -93,5 +93,5 @@
   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 n hd (%m r xs. r(tl(xs)))"
+  nth_def  "nth(n) == nat_rec hd (%m r xs. r(tl(xs))) n"
 end