--- a/NEWS Thu Mar 03 09:22:35 2005 +0100
+++ b/NEWS Thu Mar 03 12:43:01 2005 +0100
@@ -10,6 +10,37 @@
Library.OPTION: Isabelle now uses the standard option type. The
functions the, is_some, is_none, etc. are still in Library, but
the constructors are now SOME and NONE instead of Some and None.
+ They throw the exception Option.
+
+* The exception LIST is no more, the standard exceptions Empty and
+ Subscript, as well as Library.UnequalLengths are used instead. This
+ means that function like Library.hd and Library.tl are gone, as the
+ standard hd and tl functions suffice.
+
+ A number of functions, specifically those in the LIBRARY_CLOSED
+ signature, are now no longer exported to the top ML level, as they
+ are variants of standard functions. The following suggests how
+ one can translate existing code:
+
+ the x = valOf x
+ if_none x y = getOpt(x,y)
+ is_some x = isSome x
+ apsome f x = Option.map f x
+ rev_append xs ys = List.revAppend(xs,ys)
+ nth_elem(i,xs) = List.nth(xs,i)
+ last_elem xs = List.last xs
+ flat xss = List.concat xss
+ seq fs = app fs
+ partition P xs = List.partition P xs
+ filter P xs = List.filter P xs
+ mapfilter f xs = List.mapPartial f xs
+
+ The final four functions, take, drop, foldl, and foldr, are somewhat
+ more complicated (especially the semantics of take and drop differ
+ from the standard).
+
+ A simple solution to broken code is to include "open Library" at the
+ beginning of a structure. Everything after that will be as before.
* Document preparation: new antiquotations @{lhs thm} and @{rhs thm}
printing the lhs/rhs of definitions, equations, inequations etc.