# HG changeset patch
# User haftmann
# Date 1135344808 -3600
# Node ID 1b96c86711627916aa8860d497142f1b4e30cd6a
# Parent  00190b1fa5b378e2d0d5760b0f53d7b23dd08dcf
is_prefix

diff -r 00190b1fa5b3 -r 1b96c8671162 NEWS
--- a/NEWS	Thu Dec 22 19:08:15 2005 +0100
+++ b/NEWS	Fri Dec 23 14:33:28 2005 +0100
@@ -240,6 +240,13 @@
 * Pure/General: name_mangler.ML provides a functor for generic name
 mangling (bijective mapping from any expression values to strings).
 
+* Pure/library:
+
+  val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool
+
+  replacing infix "prefix" and various individual isomorphic functions scattered
+  among an amount of ML modules.
+
 * Pure/General: rat.ML implements rational numbers.
 
 * Pure: several functions of signature "... -> theory -> theory * ..."