# HG changeset patch
# User haftmann
# Date 1130772915 -3600
# Node ID dba086ed50cb4d1d7d3b7383f8a241c79b8cfc45
# Parent  652c95961a8b8befa4a52637d128ab73d6b8d6c1
nth_*, fold_index refined

diff -r 652c95961a8b -r dba086ed50cb NEWS
--- a/NEWS	Mon Oct 31 16:00:15 2005 +0100
+++ b/NEWS	Mon Oct 31 16:35:15 2005 +0100
@@ -94,6 +94,18 @@
 * Library: new module Pure/General/rat.ML implementing rational numbers,
 replacing the former functions in the Isabelle library.
 
+* Library: indexed lists - some functions in the Isabelle library
+treating lists over 'a as finite mappings from [0...n] to 'a
+have been given more convenient names and signatures reminiscent
+of similar functions for alists, tables, etc:
+
+  val nth: 'a list -> int -> 'a 
+  val nth_update: int * 'a -> 'a list -> 'a list
+  val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list
+  val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
+
+Note that fold_index starts counting at index 0, not 1 like foldln used to.
+
 * Pure: primitive rule lift_rule now takes goal cterm instead of an
 actual goal state (thm).  Use Thm.lift_rule (Thm.cgoal_of st i) to
 achieve the old behaviour.