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

NEWS

changeset 62017 | 038ee85c95e4 |

parent 62016 | 740c70a21523 |

child 62026 | ea3b1b0413b4 |

1.1 --- a/NEWS Thu Dec 31 21:06:09 2015 +0100 1.2 +++ b/NEWS Thu Dec 31 21:24:58 2015 +0100 1.3 @@ -9,6 +9,18 @@ 1.4 1.5 *** General *** 1.6 1.7 +* Former "xsymbols" syntax with Isabelle symbols is used by default, 1.8 +without any special print mode. Important ASCII replacement syntax 1.9 +remains available under print mode "ASCII", but less important syntax 1.10 +has been removed (see below). 1.11 + 1.12 +* Support for more arrow symbols, with rendering in LaTeX and 1.13 +Isabelle fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow> 1.14 + 1.15 +* Syntax for formal comments "-- text" now also supports the symbolic 1.16 +form "\<comment> text". Command-line tool "isabelle update_cartouches -c" helps 1.17 +to update old sources. 1.18 + 1.19 * Toplevel theorem statements have been simplified as follows: 1.20 1.21 theorems ~> lemmas 1.22 @@ -22,31 +34,9 @@ 1.23 * Toplevel theorem statement 'proposition' is another alias for 1.24 'theorem'. 1.25 1.26 -* Syntax for formal comments "-- text" now also supports the symbolic 1.27 -form "\<comment> text". Command-line tool "isabelle update_cartouches -c" helps 1.28 -to update old sources. 1.29 - 1.30 -* Former "xsymbols" syntax with Isabelle symbols is used by default, 1.31 -without any special print mode. Important ASCII replacement syntax 1.32 -remains available under print mode "ASCII", but less important syntax 1.33 -has been removed (see below). 1.34 - 1.35 -* Support for more arrow symbols, with rendering in LaTeX and 1.36 -Isabelle fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow> 1.37 - 1.38 1.39 *** Prover IDE -- Isabelle/Scala/jEdit *** 1.40 1.41 -* Completion of symbols via prefix of \<name> or \<^name> or \name is 1.42 -always possible, independently of the language context. It is never 1.43 -implicit: a popup will show up unconditionally. 1.44 - 1.45 -* Additional abbreviations for syntactic completion may be specified in 1.46 -$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs. 1.47 - 1.48 -* Improved scheduling for urgent print tasks (e.g. command state output, 1.49 -interactive queries) wrt. long-running background tasks. 1.50 - 1.51 * IDE support for the source-level debugger of Poly/ML, to work with 1.52 Isabelle/ML and official Standard ML. Configuration option "ML_debugger" 1.53 and commands 'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug', 1.54 @@ -56,9 +46,6 @@ 1.55 At least one Debugger view needs to be active to have any effect on the 1.56 running ML program. 1.57 1.58 -* The main Isabelle executable is managed as single-instance Desktop 1.59 -application uniformly on all platforms: Linux, Windows, Mac OS X. 1.60 - 1.61 * The State panel manages explicit proof state output, with dynamic 1.62 auto-update according to cursor movement. Alternatively, the jEdit 1.63 action "isabelle.update-state" (shortcut S+ENTER) triggers manual 1.64 @@ -80,6 +67,17 @@ 1.65 due to ad-hoc updates by auxiliary GUI components, such as the State 1.66 panel. 1.67 1.68 +* Improved scheduling for urgent print tasks (e.g. command state output, 1.69 +interactive queries) wrt. long-running background tasks. 1.70 + 1.71 +* Completion of symbols via prefix of \<name> or \<^name> or \name is 1.72 +always possible, independently of the language context. It is never 1.73 +implicit: a popup will show up unconditionally. 1.74 + 1.75 +* Additional abbreviations for syntactic completion may be specified in 1.76 +$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs, with 1.77 +support for simple templates using ASCII 007 (bell) as placeholder. 1.78 + 1.79 * Action "isabelle-emph" (with keyboard shortcut C+e LEFT) controls 1.80 emphasized text style; the effect is visible in document output, not in 1.81 the editor. 1.82 @@ -87,15 +85,18 @@ 1.83 * Action "isabelle-reset" now uses keyboard shortcut C+e BACK_SPACE, 1.84 instead of former C+e LEFT. 1.85 1.86 -* New command-line tool "isabelle jedit_client" allows to connect to an 1.87 -already running Isabelle/jEdit process. This achieves the effect of 1.88 -single-instance applications seen on common GUI desktops. 1.89 - 1.90 * The command-line tool "isabelle jedit" and the isabelle.Main 1.91 application wrapper threat the default $USER_HOME/Scratch.thy more 1.92 uniformly, and allow the dummy file argument ":" to open an empty buffer 1.93 instead. 1.94 1.95 +* New command-line tool "isabelle jedit_client" allows to connect to an 1.96 +already running Isabelle/jEdit process. This achieves the effect of 1.97 +single-instance applications seen on common GUI desktops. 1.98 + 1.99 +* The main Isabelle executable is managed as single-instance Desktop 1.100 +application uniformly on all platforms: Linux, Windows, Mac OS X. 1.101 + 1.102 * The default look-and-feel for Linux is the traditional "Metal", which 1.103 works better with GUI scaling for very high-resolution displays (e.g. 1.104 4K). Moreover, it is generally more robust than "Nimbus". 1.105 @@ -103,6 +104,21 @@ 1.106 1.107 *** Document preparation *** 1.108 1.109 +* Commands 'paragraph' and 'subparagraph' provide additional section 1.110 +headings. Thus there are 6 levels of standard headings, as in HTML. 1.111 + 1.112 +* Command 'text_raw' has been clarified: input text is processed as in 1.113 +'text' (with antiquotations and control symbols). The key difference is 1.114 +the lack of the surrounding isabelle markup environment in output. 1.115 + 1.116 +* Text is structured in paragraphs and nested lists, using notation that 1.117 +is similar to Markdown. The control symbols for list items are as 1.118 +follows: 1.119 + 1.120 + \<^item> itemize 1.121 + \<^enum> enumerate 1.122 + \<^descr> description 1.123 + 1.124 * There is a new short form for antiquotations with a single argument 1.125 that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and 1.126 \<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}. 1.127 @@ -110,18 +126,6 @@ 1.128 standard Isabelle fonts provide glyphs to render important control 1.129 symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>". 1.130 1.131 -* Antiquotation @{theory_text} prints uninterpreted theory source text 1.132 -(outer syntax with command keywords etc.). This may be used in the short 1.133 -form \<^theory_text>\<open>...\<close>. @{theory_text [display]} supports option "indent". 1.134 - 1.135 -* @{verbatim [display]} supports option "indent". 1.136 - 1.137 -* Antiquotation @{doc ENTRY} provides a reference to the given 1.138 -documentation, with a hyperlink in the Prover IDE. 1.139 - 1.140 -* Antiquotations @{command}, @{method}, @{attribute} print checked 1.141 -entities of the Isar language. 1.142 - 1.143 * Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with 1.144 corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using 1.145 standard LaTeX macros of the same names. 1.146 @@ -138,44 +142,32 @@ 1.147 argument where they are really intended, e.g. @{text \<open>"foo"\<close>}. Initial 1.148 or terminal spaces are ignored. 1.149 1.150 +* Antiquotations @{emph} and @{bold} output LaTeX source recursively, 1.151 +adding appropriate text style markup. These may be used in the short 1.152 +form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>. 1.153 + 1.154 +* Document antiquotation @{footnote} outputs LaTeX source recursively, 1.155 +marked as \footnote{}. This may be used in the short form \<^footnote>\<open>...\<close>. 1.156 + 1.157 +* Antiquotation @{verbatim [display]} supports option "indent". 1.158 + 1.159 +* Antiquotation @{theory_text} prints uninterpreted theory source text 1.160 +(outer syntax with command keywords etc.). This may be used in the short 1.161 +form \<^theory_text>\<open>...\<close>. @{theory_text [display]} supports option "indent". 1.162 + 1.163 +* Antiquotation @{doc ENTRY} provides a reference to the given 1.164 +documentation, with a hyperlink in the Prover IDE. 1.165 + 1.166 +* Antiquotations @{command}, @{method}, @{attribute} print checked 1.167 +entities of the Isar language. 1.168 + 1.169 * HTML presentation uses the standard IsabelleText font and Unicode 1.170 rendering of Isabelle symbols like Isabelle/Scala/jEdit. The former 1.171 print mode "HTML" loses its special meaning. 1.172 1.173 -* Commands 'paragraph' and 'subparagraph' provide additional section 1.174 -headings. Thus there are 6 levels of standard headings, as in HTML. 1.175 - 1.176 -* Text is structured in paragraphs and nested lists, using notation that 1.177 -is similar to Markdown. The control symbols for list items are as 1.178 -follows: 1.179 - 1.180 - \<^item> itemize 1.181 - \<^enum> enumerate 1.182 - \<^descr> description 1.183 - 1.184 -* Command 'text_raw' has been clarified: input text is processed as in 1.185 -'text' (with antiquotations and control symbols). The key difference is 1.186 -the lack of the surrounding isabelle markup environment in output. 1.187 - 1.188 -* Document antiquotations @{emph} and @{bold} output LaTeX source 1.189 -recursively, adding appropriate text style markup. These may be used in 1.190 -the short form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>. 1.191 - 1.192 -* Document antiquotation @{footnote} outputs LaTeX source recursively, 1.193 -marked as \footnote{}. This may be used in the short form \<^footnote>\<open>...\<close>. 1.194 - 1.195 1.196 *** Isar *** 1.197 1.198 -* Command 'obtain' binds term abbreviations (via 'is' patterns) in the 1.199 -proof body as well, abstracted over relevant parameters. 1.200 - 1.201 -* Improved type-inference for theorem statement 'obtains': separate 1.202 -parameter scope for of each clause. 1.203 - 1.204 -* Term abbreviations via 'is' patterns also work for schematic 1.205 -statements: result is abstracted over unknowns. 1.206 - 1.207 * Local goals ('have', 'show', 'hence', 'thus') allow structured 1.208 rule statements like fixes/assumes/shows in theorem specifications, but 1.209 the notation is postfix with keywords 'if' (or 'when') and 'for'. For 1.210 @@ -234,9 +226,6 @@ 1.211 1.212 show "C x" when "A x" "B x" for x 1.213 1.214 -* New command 'supply' supports fact definitions during goal refinement 1.215 -('apply' scripts). 1.216 - 1.217 * New command 'consider' states rules for generalized elimination and 1.218 case splitting. This is like a toplevel statement "theorem obtains" used 1.219 within a proof body; or like a multi-branch 'obtain' without activation 1.220 @@ -274,11 +263,36 @@ 1.221 is still available as legacy for some time. Documentation now explains 1.222 '..' more accurately as "by standard" instead of "by rule". 1.223 1.224 +* Nesting of Isar goal structure has been clarified: the context after 1.225 +the initial backwards refinement is retained for the whole proof, within 1.226 +all its context sections (as indicated via 'next'). This is e.g. 1.227 +relevant for 'using', 'including', 'supply': 1.228 + 1.229 + have "A \<and> A" if a: A for A 1.230 + supply [simp] = a 1.231 + proof 1.232 + show A by simp 1.233 + next 1.234 + show A by simp 1.235 + qed 1.236 + 1.237 +* Command 'obtain' binds term abbreviations (via 'is' patterns) in the 1.238 +proof body as well, abstracted over relevant parameters. 1.239 + 1.240 +* Improved type-inference for theorem statement 'obtains': separate 1.241 +parameter scope for of each clause. 1.242 + 1.243 +* Term abbreviations via 'is' patterns also work for schematic 1.244 +statements: result is abstracted over unknowns. 1.245 + 1.246 * Command 'subgoal' allows to impose some structure on backward 1.247 refinements, to avoid proof scripts degenerating into long of 'apply' 1.248 sequences. Further explanations and examples are given in the isar-ref 1.249 manual. 1.250 1.251 +* Command 'supply' supports fact definitions during goal refinement 1.252 +('apply' scripts). 1.253 + 1.254 * Proof method "goal_cases" turns the current subgoals into cases within 1.255 the context; the conclusion is bound to variable ?case in each case. For 1.256 example: 1.257 @@ -308,18 +322,8 @@ 1.258 "goals" achieves a similar effect within regular Isar; often it can be 1.259 done more adequately by other means (e.g. 'consider'). 1.260 1.261 -* Nesting of Isar goal structure has been clarified: the context after 1.262 -the initial backwards refinement is retained for the whole proof, within 1.263 -all its context sections (as indicated via 'next'). This is e.g. 1.264 -relevant for 'using', 'including', 'supply': 1.265 - 1.266 - have "A \<and> A" if a: A for A 1.267 - supply [simp] = a 1.268 - proof 1.269 - show A by simp 1.270 - next 1.271 - show A by simp 1.272 - qed 1.273 +* The vacuous fact "TERM x" may be established "by fact" or as `TERM x` 1.274 +as well, not just "by this" or "." as before. 1.275 1.276 * Method "sleep" succeeds after a real-time delay (in seconds). This is 1.277 occasionally useful for demonstration and testing purposes. 1.278 @@ -333,17 +337,16 @@ 1.279 INCOMPATIBILITY, remove '!' and add '?' as required. 1.280 1.281 * Keyword 'rewrites' identifies rewrite morphisms in interpretation 1.282 -commands. Previously, the keyword was 'where'. INCOMPATIBILITY. 1.283 +commands. Previously, the keyword was 'where'. INCOMPATIBILITY. 1.284 1.285 * More gentle suppression of syntax along locale morphisms while 1.286 -printing terms. Previously 'abbreviation' and 'notation' declarations 1.287 -would be suppressed for morphisms except term identity. Now 1.288 +printing terms. Previously 'abbreviation' and 'notation' declarations 1.289 +would be suppressed for morphisms except term identity. Now 1.290 'abbreviation' is also kept for morphims that only change the involved 1.291 -parameters, and only 'notation' is suppressed. This can be of great 1.292 -help when working with complex locale hierarchies, because proof 1.293 -states are displayed much more succinctly. It also means that only 1.294 -notation needs to be redeclared if desired, as illustrated by this 1.295 -example: 1.296 +parameters, and only 'notation' is suppressed. This can be of great help 1.297 +when working with complex locale hierarchies, because proof states are 1.298 +displayed much more succinctly. It also means that only notation needs 1.299 +to be redeclared if desired, as illustrated by this example: 1.300 1.301 locale struct = fixes composition :: "'a => 'a => 'a" (infixl "\<cdot>" 65) 1.302 begin 1.303 @@ -369,11 +372,8 @@ 1.304 * Command 'print_definitions' prints dependencies of definitional 1.305 specifications. This functionality used to be part of 'print_theory'. 1.306 1.307 -* The vacuous fact "TERM x" may be established "by fact" or as `TERM x` 1.308 -as well, not just "by this" or "." as before. 1.309 - 1.310 * Configuration option rule_insts_schematic has been discontinued 1.311 -(intermediate legacy feature in Isabelle2015). INCOMPATIBILITY. 1.312 +(intermediate legacy feature in Isabelle2015). INCOMPATIBILITY. 1.313 1.314 * Abbreviations in type classes now carry proper sort constraint. 1.315 Rare INCOMPATIBILITY in situations where the previous misbehaviour 1.316 @@ -386,9 +386,71 @@ 1.317 1.318 *** HOL *** 1.319 1.320 -* Combinator to represent case distinction on products is named "case_prod", 1.321 -uniformly, discontinuing any input aliasses. Very popular theorem aliasses 1.322 -have been retained. 1.323 +* The 'typedef' command has been upgraded from a partially checked 1.324 +"axiomatization", to a full definitional specification that takes the 1.325 +global collection of overloaded constant / type definitions into 1.326 +account. Type definitions with open dependencies on overloaded 1.327 +definitions need to be specified as "typedef (overloaded)". This 1.328 +provides extra robustness in theory construction. Rare INCOMPATIBILITY. 1.329 + 1.330 +* Qualification of various formal entities in the libraries is done more 1.331 +uniformly via "context begin qualified definition ... end" instead of 1.332 +old-style "hide_const (open) ...". Consequently, both the defined 1.333 +constant and its defining fact become qualified, e.g. Option.is_none and 1.334 +Option.is_none_def. Occasional INCOMPATIBILITY in applications. 1.335 + 1.336 +* Some old and rarely used ASCII replacement syntax has been removed. 1.337 +INCOMPATIBILITY, standard syntax with symbols should be used instead. 1.338 +The subsequent commands help to reproduce the old forms, e.g. to 1.339 +simplify porting old theories: 1.340 + 1.341 + notation iff (infixr "<->" 25) 1.342 + 1.343 + notation Times (infixr "<*>" 80) 1.344 + 1.345 + type_notation Map.map (infixr "~=>" 0) 1.346 + notation Map.map_comp (infixl "o'_m" 55) 1.347 + 1.348 + type_notation FinFun.finfun ("(_ =>f /_)" [22, 21] 21) 1.349 + 1.350 + notation FuncSet.funcset (infixr "->" 60) 1.351 + notation FuncSet.extensional_funcset (infixr "->\<^sub>E" 60) 1.352 + 1.353 + notation Omega_Words_Fun.conc (infixr "conc" 65) 1.354 + 1.355 + notation Preorder.equiv ("op ~~") 1.356 + and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50) 1.357 + 1.358 + notation (in topological_space) tendsto (infixr "--->" 55) 1.359 + notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60) 1.360 + notation LIM ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) 1.361 + 1.362 + notation NSA.approx (infixl "@=" 50) 1.363 + notation NSLIMSEQ ("((_)/ ----NS> (_))" [60, 60] 60) 1.364 + notation NSLIM ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) 1.365 + 1.366 +* The alternative notation "\<Colon>" for type and sort constraints has been 1.367 +removed: in LaTeX document output it looks the same as "::". 1.368 +INCOMPATIBILITY, use plain "::" instead. 1.369 + 1.370 +* Commands 'inductive' and 'inductive_set' work better when names for 1.371 +intro rules are omitted: the "cases" and "induct" rules no longer 1.372 +declare empty case_names, but no case_names at all. This allows to use 1.373 +numbered cases in proofs, without requiring method "goal_cases". 1.374 + 1.375 +* Inductive definitions ('inductive', 'coinductive', etc.) expose 1.376 +low-level facts of the internal construction only if the option 1.377 +"inductive_defs" is enabled. This refers to the internal predicate 1.378 +definition and its monotonicity result. Rare INCOMPATIBILITY. 1.379 + 1.380 +* Recursive function definitions ('fun', 'function', 'partial_function') 1.381 +expose low-level facts of the internal construction only if the option 1.382 +"function_defs" is enabled. Rare INCOMPATIBILITY. 1.383 + 1.384 +* Combinator to represent case distinction on products is named 1.385 +"case_prod", uniformly, discontinuing any input aliasses. Very popular 1.386 +theorem aliasses have been retained. 1.387 + 1.388 Consolidated facts: 1.389 PairE ~> prod.exhaust 1.390 Pair_eq ~> prod.inject 1.391 @@ -425,36 +487,21 @@ 1.392 split_rsp ~> case_prod_rsp 1.393 curry_split ~> curry_case_prod 1.394 split_curry ~> case_prod_curry 1.395 + 1.396 Changes in structure HOLogic: 1.397 split_const ~> case_prod_const 1.398 mk_split ~> mk_case_prod 1.399 mk_psplits ~> mk_ptupleabs 1.400 strip_psplits ~> strip_ptupleabs 1.401 -INCOMPATIBILITY. 1.402 - 1.403 -* Commands 'inductive' and 'inductive_set' work better when names for 1.404 -intro rules are omitted: the "cases" and "induct" rules no longer 1.405 -declare empty case_names, but no case_names at all. This allows to use 1.406 -numbered cases in proofs, without requiring method "goal_cases". 1.407 - 1.408 -* The 'typedef' command has been upgraded from a partially checked 1.409 -"axiomatization", to a full definitional specification that takes the 1.410 -global collection of overloaded constant / type definitions into 1.411 -account. Type definitions with open dependencies on overloaded 1.412 -definitions need to be specified as "typedef (overloaded)". This 1.413 -provides extra robustness in theory construction. Rare INCOMPATIBILITY. 1.414 - 1.415 -* Qualification of various formal entities in the libraries is done more 1.416 -uniformly via "context begin qualified definition ... end" instead of 1.417 -old-style "hide_const (open) ...". Consequently, both the defined 1.418 -constant and its defining fact become qualified, e.g. Option.is_none and 1.419 -Option.is_none_def. Occasional INCOMPATIBILITY in applications. 1.420 - 1.421 -* The coercions to type 'real' have been reorganised. The function 'real' 1.422 -is no longer overloaded, but has type 'nat => real' and abbreviates 1.423 -of_nat for that type. Also 'real_of_int :: int => real' abbreviates 1.424 -of_int for that type. Other overloaded instances of 'real' have been 1.425 -replaced by 'real_of_ereal' and 'real_of_float'. 1.426 + 1.427 +INCOMPATIBILITY. 1.428 + 1.429 +* The coercions to type 'real' have been reorganised. The function 1.430 +'real' is no longer overloaded, but has type 'nat => real' and 1.431 +abbreviates of_nat for that type. Also 'real_of_int :: int => real' 1.432 +abbreviates of_int for that type. Other overloaded instances of 'real' 1.433 +have been replaced by 'real_of_ereal' and 'real_of_float'. 1.434 + 1.435 Consolidated facts (among others): 1.436 real_of_nat_le_iff -> of_nat_le_iff 1.437 real_of_nat_numeral of_nat_numeral 1.438 @@ -478,41 +525,8 @@ 1.439 floor_divide_eq_div floor_divide_of_int_eq 1.440 real_of_int_zero_cancel of_nat_eq_0_iff 1.441 ceiling_real_of_int ceiling_of_int 1.442 -INCOMPATIBILITY. 1.443 - 1.444 -* Some old and rarely used ASCII replacement syntax has been removed. 1.445 -INCOMPATIBILITY, standard syntax with symbols should be used instead. 1.446 -The subsequent commands help to reproduce the old forms, e.g. to 1.447 -simplify porting old theories: 1.448 - 1.449 - notation iff (infixr "<->" 25) 1.450 - 1.451 - notation Times (infixr "<*>" 80) 1.452 - 1.453 - type_notation Map.map (infixr "~=>" 0) 1.454 - notation Map.map_comp (infixl "o'_m" 55) 1.455 - 1.456 - type_notation FinFun.finfun ("(_ =>f /_)" [22, 21] 21) 1.457 - 1.458 - notation FuncSet.funcset (infixr "->" 60) 1.459 - notation FuncSet.extensional_funcset (infixr "->\<^sub>E" 60) 1.460 - 1.461 - notation Omega_Words_Fun.conc (infixr "conc" 65) 1.462 - 1.463 - notation Preorder.equiv ("op ~~") 1.464 - and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50) 1.465 - 1.466 - notation (in topological_space) tendsto (infixr "--->" 55) 1.467 - notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60) 1.468 - notation LIM ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) 1.469 - 1.470 - notation NSA.approx (infixl "@=" 50) 1.471 - notation NSLIMSEQ ("((_)/ ----NS> (_))" [60, 60] 60) 1.472 - notation NSLIM ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) 1.473 - 1.474 -* The alternative notation "\<Colon>" for type and sort constraints has been 1.475 -removed: in LaTeX document output it looks the same as "::". 1.476 -INCOMPATIBILITY, use plain "::" instead. 1.477 + 1.478 +INCOMPATIBILITY. 1.479 1.480 * Theory Map: lemma map_of_is_SomeD was a clone of map_of_SomeD and has 1.481 been removed. INCOMPATIBILITY. 1.482 @@ -551,38 +565,38 @@ 1.483 'transfer_prover_start' and 'transfer_prover_end'. 1.484 1.485 * Division on integers is bootstrapped directly from division on 1.486 -naturals and uses generic numeral algorithm for computations. 1.487 -Slight INCOMPATIBILITY, simproc numeral_divmod replaces and generalizes 1.488 -former simprocs binary_int_div and binary_int_mod 1.489 - 1.490 -* Tightened specification of class semiring_no_zero_divisors. Slight 1.491 +naturals and uses generic numeral algorithm for computations. Slight 1.492 +INCOMPATIBILITY, simproc numeral_divmod replaces and generalizes former 1.493 +simprocs binary_int_div and binary_int_mod 1.494 + 1.495 +* Tightened specification of class semiring_no_zero_divisors. Minor 1.496 INCOMPATIBILITY. 1.497 1.498 * Class algebraic_semidom introduces common algebraic notions of 1.499 -integral (semi)domains, particularly units. Although 1.500 -logically subsumed by fields, is is not a super class of these 1.501 -in order not to burden fields with notions that are trivial there. 1.502 - 1.503 -* Class normalization_semidom specifies canonical representants 1.504 -for equivalence classes of associated elements in an integral 1.505 -(semi)domain. This formalizes associated elements as well. 1.506 +integral (semi)domains, particularly units. Although logically subsumed 1.507 +by fields, is is not a super class of these in order not to burden 1.508 +fields with notions that are trivial there. 1.509 + 1.510 +* Class normalization_semidom specifies canonical representants for 1.511 +equivalence classes of associated elements in an integral (semi)domain. 1.512 +This formalizes associated elements as well. 1.513 1.514 * Abstract specification of gcd/lcm operations in classes semiring_gcd, 1.515 -semiring_Gcd, semiring_Lcd. Minor INCOMPATIBILITY: facts gcd_nat.commute 1.516 -and gcd_int.commute are subsumed by gcd.commute, as well as gcd_nat.assoc 1.517 -and gcd_int.assoc by gcd.assoc. 1.518 - 1.519 -* Former constants Fields.divide (_ / _) and Divides.div (_ div _) 1.520 -are logically unified to Rings.divide in syntactic type class 1.521 -Rings.divide, with infix syntax (_ div _). Infix syntax (_ / _) 1.522 -for field division is added later as abbreviation in class Fields.inverse. 1.523 -INCOMPATIBILITY, instantiations must refer to Rings.divide rather 1.524 -than the former separate constants, hence infix syntax (_ / _) is usually 1.525 -not available during instantiation. 1.526 - 1.527 -* New cancellation simprocs for boolean algebras to cancel 1.528 -complementary terms for sup and inf. For example, "sup x (sup y (- x))" 1.529 -simplifies to "top". INCOMPATIBILITY. 1.530 +semiring_Gcd, semiring_Lcd. Minor INCOMPATIBILITY: facts gcd_nat.commute 1.531 +and gcd_int.commute are subsumed by gcd.commute, as well as 1.532 +gcd_nat.assoc and gcd_int.assoc by gcd.assoc. 1.533 + 1.534 +* Former constants Fields.divide (_ / _) and Divides.div (_ div _) are 1.535 +logically unified to Rings.divide in syntactic type class Rings.divide, 1.536 +with infix syntax (_ div _). Infix syntax (_ / _) for field division is 1.537 +added later as abbreviation in class Fields.inverse. INCOMPATIBILITY, 1.538 +instantiations must refer to Rings.divide rather than the former 1.539 +separate constants, hence infix syntax (_ / _) is usually not available 1.540 +during instantiation. 1.541 + 1.542 +* New cancellation simprocs for boolean algebras to cancel complementary 1.543 +terms for sup and inf. For example, "sup x (sup y (- x))" simplifies to 1.544 +"top". INCOMPATIBILITY. 1.545 1.546 * Library/Multiset: 1.547 - Renamed multiset inclusion operators: 1.548 @@ -614,36 +628,27 @@ 1.549 less_eq_multiset_def 1.550 INCOMPATIBILITY 1.551 1.552 -* Library/Bourbaki_Witt_Fixpoint: Added formalisation of the Bourbaki-Witt 1.553 -fixpoint theorem for increasing functions in chain-complete partial 1.554 -orders. 1.555 - 1.556 -* Multivariate_Analysis/Cauchy_Integral_Thm: Contour integrals (= complex path integrals), 1.557 -Cauchy's integral theorem, winding numbers and Cauchy's integral formula, Liouville theorem, 1.558 -Fundamental Theorem of Algebra. Ported from HOL Light 1.559 - 1.560 -* Multivariate_Analysis: Added topological concepts such as connected components, 1.561 -homotopic paths and the inside or outside of a set. 1.562 - 1.563 -* Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef' 1.564 -command. Minor INCOMPATIBILITY, use 'function' instead. 1.565 - 1.566 -* Inductive definitions ('inductive', 'coinductive', etc.) expose 1.567 -low-level facts of the internal construction only if the option 1.568 -"inductive_defs" is enabled. This refers to the internal predicate 1.569 -definition and its monotonicity result. Rare INCOMPATIBILITY. 1.570 - 1.571 -* Recursive function definitions ('fun', 'function', 'partial_function') 1.572 -expose low-level facts of the internal construction only if the option 1.573 -"function_defs" is enabled. Rare INCOMPATIBILITY. 1.574 +* Library/Omega_Words_Fun: Infinite words modeled as functions nat \<Rightarrow> 'a. 1.575 + 1.576 +* Library/Bourbaki_Witt_Fixpoint: Added formalisation of the 1.577 +Bourbaki-Witt fixpoint theorem for increasing functions in 1.578 +chain-complete partial orders. 1.579 + 1.580 +* Library/Old_Recdef: discontinued obsolete 'defer_recdef' command. 1.581 +Minor INCOMPATIBILITY, use 'function' instead. 1.582 + 1.583 +* Multivariate_Analysis/Cauchy_Integral_Thm: Contour integrals (= 1.584 +complex path integrals), Cauchy's integral theorem, winding numbers and 1.585 +Cauchy's integral formula, Liouville theorem, Fundamental Theorem of 1.586 +Algebra. Ported from HOL Light 1.587 + 1.588 +* Multivariate_Analysis: Added topological concepts such as connected 1.589 +components, homotopic paths and the inside or outside of a set. 1.590 1.591 * Data_Structures: new and growing session of standard data structures. 1.592 1.593 * Imperative_HOL: obsolete theory Legacy_Mrec has been removed. 1.594 1.595 -* Library/Omega_Words_Fun: Infinite words modeled as functions nat => 1.596 -'a. 1.597 - 1.598 * HOL-Statespace: command 'statespace' uses mandatory qualifier for 1.599 import of parent, as for general 'locale' expressions. INCOMPATIBILITY, 1.600 remove '!' and add '?' as required. 1.601 @@ -651,18 +656,19 @@ 1.602 1.603 *** ML *** 1.604 1.605 +* The following combinators for low-level profiling of the ML runtime 1.606 +system are available: 1.607 + 1.608 + profile_time (*CPU time*) 1.609 + profile_time_thread (*CPU time on this thread*) 1.610 + profile_allocations (*overall heap allocations*) 1.611 + 1.612 +* Antiquotation @{undefined} or \<^undefined> inlines (raise Match). 1.613 + 1.614 * Pretty printing of Poly/ML compiler output in Isabelle has been 1.615 improved: proper treatment of break offsets and blocks with consistent 1.616 breaks. 1.617 1.618 -* Isar proof methods are based on a slightly more general type 1.619 -context_tactic, which allows to change the proof context dynamically 1.620 -(e.g. to update cases) and indicate explicit Seq.Error results. Former 1.621 -METHOD_CASES is superseded by CONTEXT_METHOD; further combinators are 1.622 -provided in src/Pure/Isar/method.ML for convenience. INCOMPATIBILITY. 1.623 - 1.624 -* Antiquotation @{undefined} or \<^undefined> inlines (raise Match). 1.625 - 1.626 * The auxiliary module Pure/display.ML has been eliminated. Its 1.627 elementary thm print operations are now in Pure/more_thm.ML and thus 1.628 called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY. 1.629 @@ -698,18 +704,26 @@ 1.630 tools, but can also cause INCOMPATIBILITY for tools that don't observe 1.631 the proof context discipline. 1.632 1.633 -* The following combinators for low-level profiling of the ML runtime 1.634 -system are available: 1.635 - 1.636 - profile_time (*CPU time*) 1.637 - profile_time_thread (*CPU time on this thread*) 1.638 - profile_allocations (*overall heap allocations*) 1.639 +* Isar proof methods are based on a slightly more general type 1.640 +context_tactic, which allows to change the proof context dynamically 1.641 +(e.g. to update cases) and indicate explicit Seq.Error results. Former 1.642 +METHOD_CASES is superseded by CONTEXT_METHOD; further combinators are 1.643 +provided in src/Pure/Isar/method.ML for convenience. INCOMPATIBILITY. 1.644 1.645 1.646 *** System *** 1.647 1.648 * Command-line tool "isabelle console" enables print mode "ASCII". 1.649 1.650 +* Command-line tool "isabelle update_then" expands old Isar command 1.651 +conflations: 1.652 + 1.653 + hence ~> then have 1.654 + thus ~> then show 1.655 + 1.656 +This syntax is more orthogonal and improves readability and 1.657 +maintainability of proofs. 1.658 + 1.659 * Global session timeout is multiplied by timeout_scale factor. This 1.660 allows to adjust large-scale tests (e.g. AFP) to overall hardware 1.661 performance. 1.662 @@ -719,22 +733,6 @@ 1.663 1.664 \<star> code: 0x0022c6 group: operator font: Deja␣Vu␣Sans␣Mono 1.665 1.666 -* Command-line tool "isabelle update_then" expands old Isar command 1.667 -conflations: 1.668 - 1.669 - hence ~> then have 1.670 - thus ~> then show 1.671 - 1.672 -This syntax is more orthogonal and improves readability and 1.673 -maintainability of proofs. 1.674 - 1.675 -* Poly/ML default platform architecture may be changed from 32bit to 1.676 -64bit via system option ML_system_64. A system restart (and rebuild) 1.677 -is required after change. 1.678 - 1.679 -* Poly/ML 5.6 runs natively on x86-windows and x86_64-windows, which 1.680 -both allow larger heap space than former x86-cygwin. 1.681 - 1.682 * Java runtime environment for x86_64-windows allows to use larger heap 1.683 space. 1.684 1.685 @@ -757,6 +755,13 @@ 1.686 * Heap images are 10-15% smaller due to less wasteful persistent theory 1.687 content (using ML type theory_id instead of theory); 1.688 1.689 +* Poly/ML default platform architecture may be changed from 32bit to 1.690 +64bit via system option ML_system_64. A system restart (and rebuild) 1.691 +is required after change. 1.692 + 1.693 +* Poly/ML 5.6 runs natively on x86-windows and x86_64-windows, which 1.694 +both allow larger heap space than former x86-cygwin. 1.695 + 1.696 1.697 1.698 New in Isabelle2015 (May 2015)