summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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 |