NEWS
changeset 17371 923ef4a8c672
parent 17275 44d8fbc2e52d
child 17385 4dcae6e62268
equal deleted inserted replaced
17370:754b7fcff03e 17371:923ef4a8c672
    17 
    17 
    18   theory <name> = <theory1> + ... + <theoryN>:
    18   theory <name> = <theory1> + ... + <theoryN>:
    19 
    19 
    20 will disappear in the next release.  Use isatool fixheaders to convert
    20 will disappear in the next release.  Use isatool fixheaders to convert
    21 existing theory files.  Note that there is no change in ancient
    21 existing theory files.  Note that there is no change in ancient
    22 non-Isar theories now, but these are likely to disappear soon.
    22 non-Isar theories now, but these will disappear soon.
    23 
    23 
    24 * Theory loader: parent theories can now also be referred to via
    24 * Theory loader: parent theories can now also be referred to via
    25 relative and absolute paths.
    25 relative and absolute paths.
    26 
    26 
    27 * Improved version of thms_containing searches for a list of criteria
    27 * Improved version of thms_containing searches for a list of criteria
   309 Moreover, the mathematically important symbolic identifier \<epsilon>
   309 Moreover, the mathematically important symbolic identifier \<epsilon>
   310 becomes available as variable, constant etc.  INCOMPATIBILITY,
   310 becomes available as variable, constant etc.  INCOMPATIBILITY,
   311 
   311 
   312 * "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x".
   312 * "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x".
   313 Similarly for all quantifiers: "ALL x > y" etc.  The x-symbol for >=
   313 Similarly for all quantifiers: "ALL x > y" etc.  The x-symbol for >=
   314 is \<ge>. New transitivity rules have been added to HOL/Orderings.thy to 
   314 is \<ge>. New transitivity rules have been added to HOL/Orderings.thy to
   315 support corresponding Isar calculations.
   315 support corresponding Isar calculations.
   316 
   316 
   317 * "{x:A. P}" abbreviates "{x. x:A & P}", and similarly for "\<in>"
   317 * "{x:A. P}" abbreviates "{x. x:A & P}", and similarly for "\<in>"
   318 instead of ":".
   318 instead of ":".
   319 
   319 
   333   {)\([^\.]*\)\.\.  ->  {\1<\.\.}
   333   {)\([^\.]*\)\.\.  ->  {\1<\.\.}
   334   \.\.\([^(}]*\)(}  ->  \.\.<\1}
   334   \.\.\([^(}]*\)(}  ->  \.\.<\1}
   335 
   335 
   336 * theory Finite_Set: changed the syntax for 'setsum', summation over
   336 * theory Finite_Set: changed the syntax for 'setsum', summation over
   337 finite sets: "setsum (%x. e) A", which used to be "\<Sum>x:A. e", is
   337 finite sets: "setsum (%x. e) A", which used to be "\<Sum>x:A. e", is
   338 now either "SUM x:A. e" or "\<Sum>x \<in> A. e". The bound variable can 
   338 now either "SUM x:A. e" or "\<Sum>x \<in> A. e". The bound variable can
   339 be a tuple pattern.
   339 be a tuple pattern.
   340 
   340 
   341 Some new syntax forms are available:
   341 Some new syntax forms are available:
   342 
   342 
   343   "\<Sum>x | P. e"      for     "setsum (%x. e) {x. P}"
   343   "\<Sum>x | P. e"      for     "setsum (%x. e) {x. P}"
   412 
   412 
   413 The following theorems have been eliminated or modified
   413 The following theorems have been eliminated or modified
   414 (INCOMPATIBILITY):
   414 (INCOMPATIBILITY):
   415 
   415 
   416   abs_eq             now named abs_of_nonneg
   416   abs_eq             now named abs_of_nonneg
   417   abs_of_ge_0        now named abs_of_nonneg 
   417   abs_of_ge_0        now named abs_of_nonneg
   418   abs_minus_eq       now named abs_of_nonpos  
   418   abs_minus_eq       now named abs_of_nonpos
   419   imp_abs_id         now named abs_of_nonneg
   419   imp_abs_id         now named abs_of_nonneg
   420   imp_abs_neg_id     now named abs_of_nonpos
   420   imp_abs_neg_id     now named abs_of_nonpos
   421   mult_pos           now named mult_pos_pos
   421   mult_pos           now named mult_pos_pos
   422   mult_pos_le        now named mult_nonneg_nonneg
   422   mult_pos_le        now named mult_nonneg_nonneg
   423   mult_pos_neg_le    now named mult_nonneg_nonpos
   423   mult_pos_neg_le    now named mult_nonneg_nonpos
   504     mapfilter f xs = List.mapPartial f xs
   504     mapfilter f xs = List.mapPartial f xs
   505 
   505 
   506 * Pure/library.ML: several combinators for linear functional
   506 * Pure/library.ML: several combinators for linear functional
   507 transformations, notably reverse application and composition:
   507 transformations, notably reverse application and composition:
   508 
   508 
   509   x |> f		f #> g
   509   x |> f                f #> g
   510   (x, y) |-> f		f #-> g
   510   (x, y) |-> f          f #-> g
   511 
   511 
   512 * Pure/library.ML: canonical list combinators fold, fold_rev, and
   512 * Pure/library.ML: canonical list combinators fold, fold_rev, and
   513 fold_map support linear functional transformations and nesting.  For
   513 fold_map support linear functional transformations and nesting.  For
   514 example:
   514 example:
   515 
   515 
   557 (both increase the runtime).
   557 (both increase the runtime).
   558 
   558 
   559 * Isar session: The initial use of ROOT.ML is now always timed,
   559 * Isar session: The initial use of ROOT.ML is now always timed,
   560 i.e. the log will show the actual process times, in contrast to the
   560 i.e. the log will show the actual process times, in contrast to the
   561 elapsed wall-clock time that the outer shell wrapper produces.
   561 elapsed wall-clock time that the outer shell wrapper produces.
   562  
   562 
   563 * Pure: structure OrdList (cf. Pure/General/ord_list.ML) provides a
   563 * Pure: structure OrdList (cf. Pure/General/ord_list.ML) provides a
   564 reasonably efficient light-weight implementation of sets as lists.
   564 reasonably efficient light-weight implementation of sets as lists.
   565 
   565 
   566 * Pure: more efficient orders for basic syntactic entities: added
   566 * Pure: more efficient orders for basic syntactic entities: added
   567 fast_string_ord, fast_indexname_ord, fast_term_ord; changed sort_ord
   567 fast_string_ord, fast_indexname_ord, fast_term_ord; changed sort_ord