NEWS
changeset 15973 5fd94d84470f
parent 15931 8d2fdcc558d1
child 15979 c81578ac2d31
     1.1 --- a/NEWS	Tue May 17 10:19:43 2005 +0200
     1.2 +++ b/NEWS	Tue May 17 10:19:44 2005 +0200
     1.3 @@ -6,41 +6,6 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 -* ML: The type Library.option is no more, along with the exception
     1.8 -  Library.OPTION: Isabelle now uses the standard option type.  The
     1.9 -  functions the, is_some, is_none, etc. are still in Library, but
    1.10 -  the constructors are now SOME and NONE instead of Some and None.
    1.11 -  They raise the exception Option.
    1.12 -
    1.13 -* ML: The exception LIST is no more, the standard exceptions Empty and
    1.14 -  Subscript, as well as Library.UnequalLengths are used instead.  This
    1.15 -  means that function like Library.hd and Library.tl are gone, as the
    1.16 -  standard hd and tl functions suffice.
    1.17 -
    1.18 -  A number of basic functions are now no longer exported to the top ML
    1.19 -  level, as they are variants of standard functions.  The following
    1.20 -  suggests how one can translate existing code:
    1.21 -
    1.22 -    the x = valOf x
    1.23 -    if_none x y = getOpt(x,y)
    1.24 -    is_some x = isSome x
    1.25 -    apsome f x = Option.map f x
    1.26 -    rev_append xs ys = List.revAppend(xs,ys)
    1.27 -    nth_elem(i,xs) = List.nth(xs,i)
    1.28 -    last_elem xs = List.last xs
    1.29 -    flat xss = List.concat xss
    1.30 -    seq fs = app fs
    1.31 -    partition P xs = List.partition P xs
    1.32 -    filter P xs = List.filter P xs
    1.33 -    mapfilter f xs = List.mapPartial f xs
    1.34 -
    1.35 -  The final four functions, take, drop, foldl, and foldr, are somewhat
    1.36 -  more complicated (especially the semantics of take and drop differ
    1.37 -  from the standard).
    1.38 -
    1.39 -  A simple solution to broken code is to include "open Library" at the
    1.40 -  beginning of a structure.  Everything after that will be as before.
    1.41 -
    1.42  * Theory headers: the new header syntax for Isar theories is
    1.43  
    1.44    theory <name>
    1.45 @@ -381,6 +346,30 @@
    1.46  
    1.47  *** ML ***
    1.48  
    1.49 +* Pure/library.ML no longer defines its own option datatype, but uses
    1.50 +  that of the SML basis, which has constructors NONE and SOME instead
    1.51 +  of None and Some, as well as exception Option.Option instead of
    1.52 +  OPTION.  The functions the, if_none, is_some, is_none have been
    1.53 +  adapted accordingly, while Option.map replaces apsome.
    1.54 +
    1.55 +* The exception LIST is no more, the standard exceptions Empty and
    1.56 +  Subscript, as well as Library.UnequalLengths are used instead.  This
    1.57 +  means that function like Library.hd and Library.tl are gone, as the
    1.58 +  standard hd and tl functions suffice.
    1.59 +
    1.60 +  A number of basic functions are now no longer exported to the ML
    1.61 +  toplevel, as they are variants of standard functions.  The following
    1.62 +  suggests how one can translate existing code:
    1.63 +
    1.64 +    rev_append xs ys = List.revAppend (xs, ys)
    1.65 +    nth_elem (i, xs) = List.nth (xs, i)
    1.66 +    last_elem xs = List.last xs
    1.67 +    flat xss = List.concat xss
    1.68 +    seq fs = app fs
    1.69 +    partition P xs = List.partition P xs
    1.70 +    filter P xs = List.filter P xs
    1.71 +    mapfilter f xs = List.mapPartial f xs
    1.72 +
    1.73  * Pure: output via the Isabelle channels of writeln/warning/error
    1.74    etc. is now passed through Output.output, with a hook for arbitrary
    1.75    transformations depending on the print_mode (cf. Output.add_mode --