summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 20 Dec 2005 22:06:00 +0100 | |

changeset 18446 | 6c558efcc754 |

parent 18445 | 74c5481a23e6 |

child 18447 | da548623916a |

tuned;

--- a/NEWS Tue Dec 20 09:02:41 2005 +0100 +++ b/NEWS Tue Dec 20 22:06:00 2005 +0100 @@ -157,44 +157,40 @@ "=" on type bool) are handled, variable names of the form "lit_<n>" are no longer reserved, significant speedup. -* Library: added theory Coinductive_List of potentially infinite lists as -greatest fixed-point. +* Library: added theory Coinductive_List of potentially infinite lists +as greatest fixed-point. *** ML *** -* Pure: functions of signature "... -> theory -> theory * ..." have been reoriented - to "... -> theory -> ... * theory" in order to allow natural usage in combination - with the ||>, ||>>, |-> and fold_map combinators. - -* Library: new module Pure/General/name_mangler providing a functor for generic - name mangling (bijective mapping from any expression values to strings). - -* SML systems: added - print: 'a -> 'a - to smlnj. PolyML provides such a function which as a side effect prints out - a string representation of its argument. By adding print to smlnj, it is possible - to use "print" for debugging purpose without breaking smlnj compatibility. - -* Library: functions map2 and fold2 with curried syntax for simultanous - mapping and folding: +* Pure/library: functions map2 and fold2 with curried syntax for +simultanous mapping and folding: + val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c -* 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: +* Pure/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. +Note that fold_index starts counting at index 0, not 1 like foldln +used to. + +* Pure/General: name_mangler.ML provides a functor for generic name +mangling (bijective mapping from any expression values to strings). + +* Pure/General: rat.ML implements rational numbers. + +* Pure: several functions of signature "... -> theory -> theory * ..." +have been reoriented to "... -> theory -> ... * theory" in order to +allow natural usage in combination with the ||>, ||>>, |-> and +fold_map combinators. * Pure: primitive rule lift_rule now takes goal cterm instead of an actual goal state (thm). Use Thm.lift_rule (Thm.cprem_of st i) to