re-arranged tuples (theory * 'a) to ('a * theory) in Pure
authorhaftmann
Fri Dec 16 16:00:58 2005 +0100 (2005-12-16)
changeset 18422875451c9d253
parent 18421 464c93701351
child 18423 d7859164447f
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
NEWS
     1.1 --- a/NEWS	Fri Dec 16 15:52:05 2005 +0100
     1.2 +++ b/NEWS	Fri Dec 16 16:00:58 2005 +0100
     1.3 @@ -163,6 +163,24 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Pure: functions of signature "... -> theory -> theory * ..." have been reoriented
     1.8 +  to "... -> theory -> ... * theory" in order to allow natural usage in combination
     1.9 +  with the ||>, ||>>, |-> and fold_map combinators.
    1.10 +
    1.11 +* Library: new module Pure/General/name_mangler providing a functor for generic
    1.12 +    name mangling (bijective mapping from any expression values to strings).
    1.13 +
    1.14 +* SML systems: added
    1.15 +    print: 'a -> 'a
    1.16 +  to smlnj. PolyML provides such a function which as a side effect prints out
    1.17 +  a string representation of its argument. By adding print to smlnj, it is possible
    1.18 +  to use "print" for debugging purpose without breaking smlnj compatibility.
    1.19 +
    1.20 +* Library: functions map2 and fold2 with curried syntax for simultanous
    1.21 +    mapping and folding:
    1.22 +    val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
    1.23 +    val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
    1.24 +
    1.25  * Library: new module Pure/General/rat.ML implementing rational numbers,
    1.26  replacing the former functions in the Isabelle library.
    1.27