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