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

NEWS

changeset 68543 | c87e1adb91af |

parent 68541 | 12b4b3bc585d |

child 68545 | 7922992c99ea |

--- a/NEWS Fri Jun 29 16:53:37 2018 +0200 +++ b/NEWS Fri Jun 29 19:50:03 2018 +0200 @@ -36,13 +36,13 @@ * The "op <infix-op>" syntax for infix operators has been replaced by "(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to be a space between the "*" and the corresponding parenthesis. -INCOMPATIBILITY. -There is an Isabelle tool "update_op" that converts theory and ML files -to the new syntax. Because it is based on regular expression matching, -the result may need a bit of manual postprocessing. Invoking "isabelle -update_op" converts all files in the current directory (recursively). -In case you want to exclude conversion of ML files (because the tool -frequently also converts ML's "op" syntax), use option "-m". +INCOMPATIBILITY, use the command-line tool "isabelle update_op" to +convert theory and ML files to the new syntax. Because it is based on +regular expression matching, the result may need a bit of manual +postprocessing. Invoking "isabelle update_op" converts all files in the +current directory (recursively). In case you want to exclude conversion +of ML files (because the tool frequently also converts ML's "op" +syntax), use option "-m". * Theory header 'abbrevs' specifications need to be separated by 'and'. INCOMPATIBILITY. @@ -207,6 +207,12 @@ Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with object-logic equality or equivalence. + +*** Pure *** + +* The inner syntax category "sort" now includes notation "_" for the +dummy sort: it is effectively ignored in type-inference. + * Rewrites clauses (keyword 'rewrites') were moved into the locale expression syntax, where they are part of locale instances. In interpretation commands rewrites clauses now need to occur before 'for' @@ -218,17 +224,11 @@ locale instances where the qualifier's sole purpose is avoiding duplicate constant declarations. -* Proof method 'simp' now supports a new modifier 'flip:' followed by a list -of theorems. Each of these theorems is removed from the simpset -(without warning if it is not there) and the symmetric version of the theorem -(i.e. lhs and rhs exchanged) is added to the simpset. -For 'auto' and friends the modifier is "simp flip:". - - -*** Pure *** - -* The inner syntax category "sort" now includes notation "_" for the -dummy sort: it is effectively ignored in type-inference. +* Proof method "simp" now supports a new modifier "flip:" followed by a +list of theorems. Each of these theorems is removed from the simpset +(without warning if it is not there) and the symmetric version of the +theorem (i.e. lhs and rhs exchanged) is added to the simpset. For "auto" +and friends the modifier is "simp flip:". *** HOL *** @@ -391,12 +391,12 @@ * Session HOL-Algebra: renamed (^) to [^] to avoid conflict with new infix/prefix notation. -* Session HOL-Algebra: Revamped with much new material. -The set of isomorphisms between two groups is now denoted iso rather than iso_set. -INCOMPATIBILITY. - -* Session HOL-Analysis: the Arg function now respects the same interval as -Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi. +* Session HOL-Algebra: revamped with much new material. The set of +isomorphisms between two groups is now denoted iso rather than iso_set. +INCOMPATIBILITY. + +* Session HOL-Analysis: the Arg function now respects the same interval +as Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi. INCOMPATIBILITY. * Session HOL-Analysis: infinite products, Moebius functions, the