summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

changeset 68547 | 549a4992222f |

parent 68532 | 7c6f812afdc4 |

parent 68545 | 7922992c99ea |

child 68548 | a22540ac7052 |

1.1 --- a/NEWS Fri Jun 29 15:22:30 2018 +0100 1.2 +++ b/NEWS Fri Jun 29 22:14:33 2018 +0200 1.3 @@ -19,6 +19,11 @@ 1.4 FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for 1.5 formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK". 1.6 1.7 +* Global facts need to be closed: no free variables, no hypotheses, no 1.8 +pending sort hypotheses. Rare INCOMPATIBILITY: sort hypotheses can be 1.9 +allowed via "declare [[pending_shyps]]" in the global theory context, 1.10 +but it should be reset to false afterwards. 1.11 + 1.12 * Marginal comments need to be written exclusively in the new-style form 1.13 "\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer 1.14 supported. INCOMPATIBILITY, use the command-line tool "isabelle 1.15 @@ -31,13 +36,13 @@ 1.16 * The "op <infix-op>" syntax for infix operators has been replaced by 1.17 "(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to 1.18 be a space between the "*" and the corresponding parenthesis. 1.19 -INCOMPATIBILITY. 1.20 -There is an Isabelle tool "update_op" that converts theory and ML files 1.21 -to the new syntax. Because it is based on regular expression matching, 1.22 -the result may need a bit of manual postprocessing. Invoking "isabelle 1.23 -update_op" converts all files in the current directory (recursively). 1.24 -In case you want to exclude conversion of ML files (because the tool 1.25 -frequently also converts ML's "op" syntax), use option "-m". 1.26 +INCOMPATIBILITY, use the command-line tool "isabelle update_op" to 1.27 +convert theory and ML files to the new syntax. Because it is based on 1.28 +regular expression matching, the result may need a bit of manual 1.29 +postprocessing. Invoking "isabelle update_op" converts all files in the 1.30 +current directory (recursively). In case you want to exclude conversion 1.31 +of ML files (because the tool frequently also converts ML's "op" 1.32 +syntax), use option "-m". 1.33 1.34 * Theory header 'abbrevs' specifications need to be separated by 'and'. 1.35 INCOMPATIBILITY. 1.36 @@ -80,11 +85,15 @@ 1.37 - option -A specifies an alternative ancestor session for options -R 1.38 and -S 1.39 1.40 + - option -i includes additional sessions into the name-space of 1.41 + theories 1.42 + 1.43 Examples: 1.44 isabelle jedit -R HOL-Number_Theory 1.45 isabelle jedit -R HOL-Number_Theory -A HOL 1.46 isabelle jedit -d '$AFP' -S Formal_SSA -A HOL 1.47 isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis 1.48 + isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis -i CryptHOL 1.49 1.50 * PIDE markup for session ROOT files: allows to complete session names, 1.51 follow links to theories and document files etc. 1.52 @@ -119,14 +128,14 @@ 1.53 plain-text document draft. Both are available via the menu "Plugins / 1.54 Isabelle". 1.55 1.56 -* Bibtex database files (.bib) are semantically checked. 1.57 - 1.58 * When loading text files, the Isabelle symbols encoding UTF-8-Isabelle 1.59 is only used if there is no conflict with existing Unicode sequences in 1.60 the file. Otherwise, the fallback encoding is plain UTF-8 and Isabelle 1.61 symbols remain in literal \<symbol> form. This avoids accidental loss of 1.62 Unicode content when saving the file. 1.63 1.64 +* Bibtex database files (.bib) are semantically checked. 1.65 + 1.66 * Update to jedit-5.5.0, the latest release. 1.67 1.68 1.69 @@ -198,6 +207,12 @@ 1.70 Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with 1.71 object-logic equality or equivalence. 1.72 1.73 + 1.74 +*** Pure *** 1.75 + 1.76 +* The inner syntax category "sort" now includes notation "_" for the 1.77 +dummy sort: it is effectively ignored in type-inference. 1.78 + 1.79 * Rewrites clauses (keyword 'rewrites') were moved into the locale 1.80 expression syntax, where they are part of locale instances. In 1.81 interpretation commands rewrites clauses now need to occur before 'for' 1.82 @@ -209,17 +224,11 @@ 1.83 locale instances where the qualifier's sole purpose is avoiding 1.84 duplicate constant declarations. 1.85 1.86 -* Proof method 'simp' now supports a new modifier 'flip:' followed by a list 1.87 -of theorems. Each of these theorems is removed from the simpset 1.88 -(without warning if it is not there) and the symmetric version of the theorem 1.89 -(i.e. lhs and rhs exchanged) is added to the simpset. 1.90 -For 'auto' and friends the modifier is "simp flip:". 1.91 - 1.92 - 1.93 -*** Pure *** 1.94 - 1.95 -* The inner syntax category "sort" now includes notation "_" for the 1.96 -dummy sort: it is effectively ignored in type-inference. 1.97 +* Proof method "simp" now supports a new modifier "flip:" followed by a 1.98 +list of theorems. Each of these theorems is removed from the simpset 1.99 +(without warning if it is not there) and the symmetric version of the 1.100 +theorem (i.e. lhs and rhs exchanged) is added to the simpset. For "auto" 1.101 +and friends the modifier is "simp flip:". 1.102 1.103 1.104 *** HOL *** 1.105 @@ -382,12 +391,12 @@ 1.106 * Session HOL-Algebra: renamed (^) to [^] to avoid conflict with new 1.107 infix/prefix notation. 1.108 1.109 -* Session HOL-Algebra: Revamped with much new material. 1.110 -The set of isomorphisms between two groups is now denoted iso rather than iso_set. 1.111 -INCOMPATIBILITY. 1.112 - 1.113 -* Session HOL-Analysis: the Arg function now respects the same interval as 1.114 -Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi. 1.115 +* Session HOL-Algebra: revamped with much new material. The set of 1.116 +isomorphisms between two groups is now denoted iso rather than iso_set. 1.117 +INCOMPATIBILITY. 1.118 + 1.119 +* Session HOL-Analysis: the Arg function now respects the same interval 1.120 +as Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi. 1.121 INCOMPATIBILITY. 1.122 1.123 * Session HOL-Analysis: the functions zorder, zer_poly, porder and pol_poly have been redefined. 1.124 @@ -398,10 +407,9 @@ 1.125 Riemann mapping theorem, the Vitali covering theorem, 1.126 change-of-variables results for integration and measures. 1.127 1.128 -* Session HOL-Types_To_Sets: more tool support 1.129 -(unoverload_type combines internalize_sorts and unoverload) and larger 1.130 -experimental application (type based linear algebra transferred to linear 1.131 -algebra on subspaces). 1.132 +* Session HOL-Types_To_Sets: more tool support (unoverload_type combines 1.133 +internalize_sorts and unoverload) and larger experimental application 1.134 +(type based linear algebra transferred to linear algebra on subspaces). 1.135 1.136 1.137 *** ML ***