author | wenzelm |

Fri Jun 29 19:50:03 2018 +0200 (17 months ago) | |

changeset 68543 | c87e1adb91af |

parent 68542 | 02df6c68a8cb |

child 68544 | 8285fa53bfac |

misc tuning for release;

1.1 --- a/NEWS Fri Jun 29 16:53:37 2018 +0200 1.2 +++ b/NEWS Fri Jun 29 19:50:03 2018 +0200 1.3 @@ -36,13 +36,13 @@ 1.4 * The "op <infix-op>" syntax for infix operators has been replaced by 1.5 "(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to 1.6 be a space between the "*" and the corresponding parenthesis. 1.7 -INCOMPATIBILITY. 1.8 -There is an Isabelle tool "update_op" that converts theory and ML files 1.9 -to the new syntax. Because it is based on regular expression matching, 1.10 -the result may need a bit of manual postprocessing. Invoking "isabelle 1.11 -update_op" converts all files in the current directory (recursively). 1.12 -In case you want to exclude conversion of ML files (because the tool 1.13 -frequently also converts ML's "op" syntax), use option "-m". 1.14 +INCOMPATIBILITY, use the command-line tool "isabelle update_op" to 1.15 +convert theory and ML files to the new syntax. Because it is based on 1.16 +regular expression matching, the result may need a bit of manual 1.17 +postprocessing. Invoking "isabelle update_op" converts all files in the 1.18 +current directory (recursively). In case you want to exclude conversion 1.19 +of ML files (because the tool frequently also converts ML's "op" 1.20 +syntax), use option "-m". 1.21 1.22 * Theory header 'abbrevs' specifications need to be separated by 'and'. 1.23 INCOMPATIBILITY. 1.24 @@ -207,6 +207,12 @@ 1.25 Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with 1.26 object-logic equality or equivalence. 1.27 1.28 + 1.29 +*** Pure *** 1.30 + 1.31 +* The inner syntax category "sort" now includes notation "_" for the 1.32 +dummy sort: it is effectively ignored in type-inference. 1.33 + 1.34 * Rewrites clauses (keyword 'rewrites') were moved into the locale 1.35 expression syntax, where they are part of locale instances. In 1.36 interpretation commands rewrites clauses now need to occur before 'for' 1.37 @@ -218,17 +224,11 @@ 1.38 locale instances where the qualifier's sole purpose is avoiding 1.39 duplicate constant declarations. 1.40 1.41 -* Proof method 'simp' now supports a new modifier 'flip:' followed by a list 1.42 -of theorems. Each of these theorems is removed from the simpset 1.43 -(without warning if it is not there) and the symmetric version of the theorem 1.44 -(i.e. lhs and rhs exchanged) is added to the simpset. 1.45 -For 'auto' and friends the modifier is "simp flip:". 1.46 - 1.47 - 1.48 -*** Pure *** 1.49 - 1.50 -* The inner syntax category "sort" now includes notation "_" for the 1.51 -dummy sort: it is effectively ignored in type-inference. 1.52 +* Proof method "simp" now supports a new modifier "flip:" followed by a 1.53 +list of theorems. Each of these theorems is removed from the simpset 1.54 +(without warning if it is not there) and the symmetric version of the 1.55 +theorem (i.e. lhs and rhs exchanged) is added to the simpset. For "auto" 1.56 +and friends the modifier is "simp flip:". 1.57 1.58 1.59 *** HOL *** 1.60 @@ -391,12 +391,12 @@ 1.61 * Session HOL-Algebra: renamed (^) to [^] to avoid conflict with new 1.62 infix/prefix notation. 1.63 1.64 -* Session HOL-Algebra: Revamped with much new material. 1.65 -The set of isomorphisms between two groups is now denoted iso rather than iso_set. 1.66 -INCOMPATIBILITY. 1.67 - 1.68 -* Session HOL-Analysis: the Arg function now respects the same interval as 1.69 -Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi. 1.70 +* Session HOL-Algebra: revamped with much new material. The set of 1.71 +isomorphisms between two groups is now denoted iso rather than iso_set. 1.72 +INCOMPATIBILITY. 1.73 + 1.74 +* Session HOL-Analysis: the Arg function now respects the same interval 1.75 +as Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi. 1.76 INCOMPATIBILITY. 1.77 1.78 * Session HOL-Analysis: infinite products, Moebius functions, the