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

author | wenzelm |

Tue, 13 Sep 2005 22:49:12 +0200 | |

changeset 17371 | 923ef4a8c672 |

parent 17370 | 754b7fcff03e |

child 17372 | d73f67e90a95 |

tuned;

--- a/NEWS Tue Sep 13 22:21:06 2005 +0200 +++ b/NEWS Tue Sep 13 22:49:12 2005 +0200 @@ -19,7 +19,7 @@ will disappear in the next release. Use isatool fixheaders to convert existing theory files. Note that there is no change in ancient -non-Isar theories now, but these are likely to disappear soon. +non-Isar theories now, but these will disappear soon. * Theory loader: parent theories can now also be referred to via relative and absolute paths. @@ -311,7 +311,7 @@ * "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x". Similarly for all quantifiers: "ALL x > y" etc. The x-symbol for >= -is \<ge>. New transitivity rules have been added to HOL/Orderings.thy to +is \<ge>. New transitivity rules have been added to HOL/Orderings.thy to support corresponding Isar calculations. * "{x:A. P}" abbreviates "{x. x:A & P}", and similarly for "\<in>" @@ -335,7 +335,7 @@ * theory Finite_Set: changed the syntax for 'setsum', summation over finite sets: "setsum (%x. e) A", which used to be "\<Sum>x:A. e", is -now either "SUM x:A. e" or "\<Sum>x \<in> A. e". The bound variable can +now either "SUM x:A. e" or "\<Sum>x \<in> A. e". The bound variable can be a tuple pattern. Some new syntax forms are available: @@ -414,8 +414,8 @@ (INCOMPATIBILITY): abs_eq now named abs_of_nonneg - abs_of_ge_0 now named abs_of_nonneg - abs_minus_eq now named abs_of_nonpos + abs_of_ge_0 now named abs_of_nonneg + abs_minus_eq now named abs_of_nonpos imp_abs_id now named abs_of_nonneg imp_abs_neg_id now named abs_of_nonpos mult_pos now named mult_pos_pos @@ -506,8 +506,8 @@ * Pure/library.ML: several combinators for linear functional transformations, notably reverse application and composition: - x |> f f #> g - (x, y) |-> f f #-> g + x |> f f #> g + (x, y) |-> f f #-> g * Pure/library.ML: canonical list combinators fold, fold_rev, and fold_map support linear functional transformations and nesting. For @@ -559,7 +559,7 @@ * Isar session: The initial use of ROOT.ML is now always timed, i.e. the log will show the actual process times, in contrast to the elapsed wall-clock time that the outer shell wrapper produces. - + * Pure: structure OrdList (cf. Pure/General/ord_list.ML) provides a reasonably efficient light-weight implementation of sets as lists.