author | wenzelm |

Wed Apr 08 11:13:53 2015 +0200 (2015-04-08) | |

changeset 59951 | 8c49daca5d9f |

parent 59950 | 364b0512ce74 |

child 59952 | 550b74e9b08c |

misc tuning for release;

1.1 --- a/NEWS Tue Apr 07 18:22:06 2015 +0200 1.2 +++ b/NEWS Wed Apr 08 11:13:53 2015 +0200 1.3 @@ -26,40 +26,35 @@ 1.4 * Command 'experiment' opens an anonymous locale context with private 1.5 naming policy. 1.6 1.7 -* Structural composition of proof methods (meth1; meth2) in Isar 1.8 -corresponds to (tac1 THEN_ALL_NEW tac2) in ML. 1.9 - 1.10 -* Generated schematic variables in standard format of exported facts are 1.11 -incremented to avoid material in the proof context. Rare 1.12 -INCOMPATIBILITY, explicit instantiation sometimes needs to refer to 1.13 -different index. 1.14 +* Command 'notepad' requires proper nesting of begin/end and its proof 1.15 +structure in the body: 'oops' is no longer supported here. Minor 1.16 +INCOMPATIBILITY, use 'sorry' instead. 1.17 + 1.18 +* Command 'named_theorems' declares a dynamic fact within the context, 1.19 +together with an attribute to maintain the content incrementally. This 1.20 +supersedes functor Named_Thms in Isabelle/ML, but with a subtle change 1.21 +of semantics due to external visual order vs. internal reverse order. 1.22 + 1.23 +* 'find_theorems': search patterns which are abstractions are 1.24 +schematically expanded before search. Search results match the naive 1.25 +expectation more closely, particularly wrt. abbreviations. 1.26 +INCOMPATIBILITY. 1.27 1.28 * Commands 'method_setup' and 'attribute_setup' now work within a local 1.29 theory context. 1.30 1.31 -* Command 'named_theorems' declares a dynamic fact within the context, 1.32 -together with an attribute to maintain the content incrementally. This 1.33 -supersedes functor Named_Thms, but with a subtle change of semantics due 1.34 -to external visual order vs. internal reverse order. 1.35 - 1.36 -* Command 'notepad' requires proper nesting of begin/end and its proof 1.37 -structure in the body: 'oops' is no longer supported here. Minor 1.38 -INCOMPATIBILITY, use 'sorry' instead. 1.39 - 1.40 * Outer syntax commands are managed authentically within the theory 1.41 context, without implicit global state. Potential for accidental 1.42 INCOMPATIBILITY, make sure that required theories are really imported. 1.43 1.44 -* 'find_theorems': search patterns which are abstractions are 1.45 -schematically expanded before search. Search results match the naive 1.46 -expectation more closely, particularly wrt. abbreviations. 1.47 -INCOMPATIBILITY. 1.48 +* Structural composition of proof methods (meth1; meth2) in Isar 1.49 +corresponds to (tac1 THEN_ALL_NEW tac2) in ML. 1.50 1.51 1.52 *** Prover IDE -- Isabelle/Scala/jEdit *** 1.53 1.54 -* Old graph browser (Java/AWT 1.0) is superseded by improved graphview 1.55 -panel, which also includes PDF output. 1.56 +* Old graph browser (Java/AWT 1.1) is superseded by improved graphview 1.57 +panel, which also produces PDF output without external tools. 1.58 1.59 * Improved folding mode "isabelle" based on Isar syntax. Alternatively, 1.60 the "sidekick" mode may be used for document structure. 1.61 @@ -79,6 +74,43 @@ 1.62 Options / Text Area). 1.63 1.64 1.65 +*** Document preparation *** 1.66 + 1.67 +* Discontinued obsolete option "document_graph": session_graph.pdf is 1.68 +produced unconditionally for HTML browser_info and PDF-LaTeX document. 1.69 + 1.70 +* Document markup commands 'chapter', 'section', 'subsection', 1.71 +'subsubsection', 'text', 'txt', 'text_raw' work uniformly in any 1.72 +context, even before the initial 'theory' command. Obsolete proof 1.73 +commands 'sect', 'subsect', 'subsubsect', 'txt_raw' have been 1.74 +discontinued, use 'section', 'subsection', 'subsubsection', 'text_raw' 1.75 +instead. The old 'header' command is still retained for some time, but 1.76 +should be replaced by 'chapter', 'section' etc. (using "isabelle 1.77 +update_header"). Minor INCOMPATIBILITY. 1.78 + 1.79 +* Diagnostic commands and document markup commands within a proof do not 1.80 +affect the command tag for output. Thus commands like 'thm' are subject 1.81 +to proof document structure, and no longer "stick out" accidentally. 1.82 +Commands 'text' and 'txt' merely differ in the LaTeX style, not their 1.83 +tags. Potential INCOMPATIBILITY in exotic situations. 1.84 + 1.85 +* System option "pretty_margin" is superseded by "thy_output_margin", 1.86 +which is also accessible via document antiquotation option "margin". 1.87 +Only the margin for document output may be changed, but not the global 1.88 +pretty printing: that is 76 for plain console output, and adapted 1.89 +dynamically in GUI front-ends. Implementations of document 1.90 +antiquotations need to observe the margin explicitly according to 1.91 +Thy_Output.string_of_margin. Minor INCOMPATIBILITY. 1.92 + 1.93 +* Official support for "tt" style variants, via \isatt{...} or 1.94 +\begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or 1.95 +verbatim environment of LaTeX is no longer used. This allows @{ML} etc. 1.96 +as argument to other macros (such as footnotes). 1.97 + 1.98 +* Document antiquotation @{verbatim} prints ASCII text literally in "tt" 1.99 +style. 1.100 + 1.101 + 1.102 *** Pure *** 1.103 1.104 * Explicit instantiation via attributes "where", "of", and proof methods 1.105 @@ -94,6 +126,11 @@ 1.106 declare rule_insts_schematic = true temporarily and update to use local 1.107 variable declarations or dummy patterns instead. 1.108 1.109 +* Generated schematic variables in standard format of exported facts are 1.110 +incremented to avoid material in the proof context. Rare 1.111 +INCOMPATIBILITY, explicit instantiation sometimes needs to refer to 1.112 +different index. 1.113 + 1.114 * Command "class_deps" takes optional sort arguments constraining 1.115 the search space. 1.116 1.117 @@ -109,43 +146,44 @@ 1.118 1.119 *** HOL *** 1.120 1.121 -* Given up separate type class no_zero_divisors in favour of fully algebraic 1.122 -semiring_no_zero_divisors. INCOMPATIBILITY. 1.123 +* Given up separate type class no_zero_divisors in favour of fully 1.124 +algebraic semiring_no_zero_divisors. INCOMPATIBILITY. 1.125 1.126 * Class linordered_semidom really requires no zero divisors. 1.127 INCOMPATIBILITY. 1.128 1.129 * Classes division_ring, field and linordered_field always demand 1.130 -`inverse 0 = 0`. Given up separate classes division_ring_inverse_zero, 1.131 -field_inverse_zero and linordered_field_inverse_zero. 1.132 -INCOMPATIBILITY. 1.133 +"inverse 0 = 0". Given up separate classes division_ring_inverse_zero, 1.134 +field_inverse_zero and linordered_field_inverse_zero. INCOMPATIBILITY. 1.135 1.136 * Type classes cancel_ab_semigroup_add / cancel_monoid_add specify 1.137 -explicit additive inverse operation. INCOMPATIBILITY. 1.138 - 1.139 -* New proof method "rewrite" (in ~~/src/HOL/Library/Rewrite) for 1.140 - single-step rewriting with subterm selection based on patterns. 1.141 - 1.142 -* The functions "sin" and "cos" are now defined for any "'{real_normed_algebra_1,banach}" 1.143 - type, so in particular on "real" and "complex" uniformly. 1.144 - Minor INCOMPATIBILITY: type constraints may be needed. 1.145 - 1.146 -* New library of properties of the complex transcendental functions sin, cos, tan, exp, 1.147 - Ln, Arctan, Arcsin, Arccos. Ported from HOL Light. 1.148 - 1.149 -* The factorial function, "fact", now has type "nat => 'a" (of a sort that admits 1.150 - numeric types including nat, int, real and complex. INCOMPATIBILITY: 1.151 - an expression such as "fact 3 = 6" may require a type constraint, and the combination 1.152 - "real (fact k)" is likely to be unsatisfactory. If a type conversion is still necessary, 1.153 - then use "of_nat (fact k)" or "real_of_nat (fact k)". 1.154 - 1.155 -* removed functions "natfloor" and "natceiling", 1.156 - use "nat o floor" and "nat o ceiling" instead. 1.157 - A few of the lemmas have been retained and adapted: in their names 1.158 - "natfloor"/"natceiling" has been replaced by "nat_floor"/"nat_ceiling". 1.159 - 1.160 -* Qualified some duplicated fact names required for boostrapping 1.161 -the type class hierarchy: 1.162 +explicit additive inverse operation. INCOMPATIBILITY. 1.163 + 1.164 +* New proof method "rewrite" (in theory ~~/src/HOL/Library/Rewrite) for 1.165 +single-step rewriting with subterm selection based on patterns. 1.166 + 1.167 +* The functions "sin" and "cos" are now defined for any 1.168 +"'{real_normed_algebra_1,banach}" type, so in particular on "real" and 1.169 +"complex" uniformly. Minor INCOMPATIBILITY: type constraints may be 1.170 +needed. 1.171 + 1.172 +* New library of properties of the complex transcendental functions sin, 1.173 +cos, tan, exp, Ln, Arctan, Arcsin, Arccos. Ported from HOL Light. 1.174 + 1.175 +* The factorial function, "fact", now has type "nat => 'a" (of a sort 1.176 +that admits numeric types including nat, int, real and complex. 1.177 +INCOMPATIBILITY: an expression such as "fact 3 = 6" may require a type 1.178 +constraint, and the combination "real (fact k)" is likely to be 1.179 +unsatisfactory. If a type conversion is still necessary, then use 1.180 +"of_nat (fact k)" or "real_of_nat (fact k)". 1.181 + 1.182 +* Removed functions "natfloor" and "natceiling", use "nat o floor" and 1.183 +"nat o ceiling" instead. A few of the lemmas have been retained and 1.184 +adapted: in their names "natfloor"/"natceiling" has been replaced by 1.185 +"nat_floor"/"nat_ceiling". 1.186 + 1.187 +* Qualified some duplicated fact names required for boostrapping the 1.188 +type class hierarchy: 1.189 ab_add_uminus_conv_diff ~> diff_conv_add_uminus 1.190 field_inverse_zero ~> inverse_zero 1.191 field_divide_inverse ~> divide_inverse 1.192 @@ -160,13 +198,7 @@ 1.193 * Fact consolidation: even_less_0_iff is subsumed by 1.194 double_add_less_zero_iff_single_add_less_zero (simp by default anyway). 1.195 1.196 -* Discontinued old-fashioned "codegen" tool. Code generation can always 1.197 -be externally triggered using an appropriate ROOT file plus a 1.198 -corresponding theory. Parametrization is possible using environment 1.199 -variables, or ML snippets in the most extreme cases. Minor 1.200 -INCOMPATIBILITY. 1.201 - 1.202 -* Add NO_MATCH-simproc, allows to check for syntactic non-equality 1.203 +* Add NO_MATCH-simproc, allows to check for syntactic non-equality. 1.204 1.205 * Generalized and consolidated some theorems concerning divsibility: 1.206 dvd_reduce ~> dvd_add_triv_right_iff 1.207 @@ -175,18 +207,17 @@ 1.208 Minor INCOMPATIBILITY. 1.209 1.210 * "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _" 1.211 -and part of HOL-Main. 1.212 +and part of theory Main. 1.213 even_def ~> even_iff_mod_2_eq_zero 1.214 INCOMPATIBILITY. 1.215 1.216 -* Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1 1.217 -Minor INCOMPATIBILITY. 1.218 +* Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1. Minor 1.219 +INCOMPATIBILITY. 1.220 1.221 * field_simps: Use NO_MATCH-simproc for distribution rules, to avoid 1.222 - non-termination in case of distributing a division. With this change 1.223 - field_simps is in some cases slightly less powerful, if it fails try 1.224 - to add algebra_simps, or use divide_simps. 1.225 -Minor INCOMPATIBILITY. 1.226 +non-termination in case of distributing a division. With this change 1.227 +field_simps is in some cases slightly less powerful, if it fails try to 1.228 +add algebra_simps, or use divide_simps. Minor INCOMPATIBILITY. 1.229 1.230 * Bootstrap of listsum as special case of abstract product over lists. 1.231 Fact rename: 1.232 @@ -194,7 +225,7 @@ 1.233 INCOMPATIBILITY. 1.234 1.235 * Command and antiquotation "value" provide different evaluation slots 1.236 -(again), where the previous strategy (nbe after ML) serves as default. 1.237 +(again), where the previous strategy (NBE after ML) serves as default. 1.238 Minor INCOMPATIBILITY. 1.239 1.240 * New (co)datatype package: 1.241 @@ -284,7 +315,7 @@ 1.242 - New option 'smt_statistics' to display statistics of the new 'smt' 1.243 method, especially runtime statistics of Z3 proof reconstruction. 1.244 1.245 -* List: renamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc 1.246 +* List: renamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc. 1.247 1.248 * New infrastructure for compiling, running, evaluating and testing 1.249 generated code in target languages in HOL/Library/Code_Test. See 1.250 @@ -330,44 +361,26 @@ 1.251 projection 1.252 1.253 1.254 -*** Document preparation *** 1.255 - 1.256 -* Discontinued obsolete option "document_graph": session_graph.pdf is 1.257 -produced unconditionally for HTML browser_info and PDF-LaTeX document. 1.258 - 1.259 -* Document markup commands 'chapter', 'section', 'subsection', 1.260 -'subsubsection', 'text', 'txt', 'text_raw' work uniformly in any 1.261 -context, even before the initial 'theory' command. Obsolete proof 1.262 -commands 'sect', 'subsect', 'subsubsect', 'txt_raw' have been 1.263 -discontinued, use 'section', 'subsection', 'subsubsection', 'text_raw' 1.264 -instead. The old 'header' command is still retained for some time, but 1.265 -should be replaced by 'chapter', 'section' etc. (using "isabelle 1.266 -update_header"). Minor INCOMPATIBILITY. 1.267 - 1.268 -* Diagnostic commands and document markup commands within a proof do not 1.269 -affect the command tag for output. Thus commands like 'thm' are subject 1.270 -to proof document structure, and no longer "stick out" accidentally. 1.271 -Commands 'text' and 'txt' merely differ in the LaTeX style, not their 1.272 -tags. Potential INCOMPATIBILITY in exotic situations. 1.273 - 1.274 -* Official support for "tt" style variants, via \isatt{...} or 1.275 -\begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or 1.276 -verbatim environment of LaTeX is no longer used. This allows @{ML} etc. 1.277 -as argument to other macros (such as footnotes). 1.278 - 1.279 -* Document antiquotation @{verbatim} prints ASCII text literally in "tt" 1.280 -style. 1.281 - 1.282 - 1.283 *** ML *** 1.284 1.285 -* Subtle change of name space policy: undeclared entries are now 1.286 -considered inaccessible, instead of accessible via the fully-qualified 1.287 -internal name. This mainly affects Name_Space.intern (and derivatives), 1.288 -which may produce an unexpected Long_Name.hidden prefix. Note that 1.289 -contempory applications use the strict Name_Space.check (and 1.290 -derivatives) instead, which is not affected by the change. Potential 1.291 -INCOMPATIBILITY in rare applications of Name_Space.intern. 1.292 +* Cartouches within ML sources are turned into values of type 1.293 +Input.source (with formal position information). 1.294 + 1.295 +* Basic combinators map, fold, fold_map, split_list, apply are available 1.296 +as parameterized antiquotations, e.g. @{map 4} for lists of quadruples. 1.297 + 1.298 +* Renamed "pairself" to "apply2", in accordance to @{apply 2}. 1.299 +INCOMPATIBILITY. 1.300 + 1.301 +* Former combinators NAMED_CRITICAL and CRITICAL for central critical 1.302 +sections have been discontinued, in favour of the more elementary 1.303 +Multithreading.synchronized and its high-level derivative 1.304 +Synchronized.var (which is usually sufficient in applications). Subtle 1.305 +INCOMPATIBILITY: synchronized access needs to be atomic and cannot be 1.306 +nested. 1.307 + 1.308 +* Synchronized.value (ML) is actually synchronized (as in Scala): 1.309 +subtle change of semantics with minimal potential for INCOMPATIBILITY. 1.310 1.311 * The main operations to certify logical entities are Thm.ctyp_of and 1.312 Thm.cterm_of with a local context; old-style global theory variants are 1.313 @@ -378,15 +391,13 @@ 1.314 INCOMPATIBILITY, need to use qualified Thm.prop_of, Thm.cterm_of, 1.315 Thm.term_of etc. 1.316 1.317 -* Former combinators NAMED_CRITICAL and CRITICAL for central critical 1.318 -sections have been discontinued, in favour of the more elementary 1.319 -Multithreading.synchronized and its high-level derivative 1.320 -Synchronized.var (which is usually sufficient in applications). Subtle 1.321 -INCOMPATIBILITY: synchronized access needs to be atomic and cannot be 1.322 -nested. 1.323 - 1.324 -* Cartouches within ML sources are turned into values of type 1.325 -Input.source (with formal position information). 1.326 +* Subtle change of name space policy: undeclared entries are now 1.327 +considered inaccessible, instead of accessible via the fully-qualified 1.328 +internal name. This mainly affects Name_Space.intern (and derivatives), 1.329 +which may produce an unexpected Long_Name.hidden prefix. Note that 1.330 +contempory applications use the strict Name_Space.check (and 1.331 +derivatives) instead, which is not affected by the change. Potential 1.332 +INCOMPATIBILITY in rare applications of Name_Space.intern. 1.333 1.334 * Proper context for various elementary tactics: assume_tac, 1.335 resolve_tac, eresolve_tac, dresolve_tac, forward_tac, match_tac, 1.336 @@ -395,16 +406,6 @@ 1.337 * Tactical PARALLEL_ALLGOALS is the most common way to refer to 1.338 PARALLEL_GOALS. 1.339 1.340 -* Basic combinators map, fold, fold_map, split_list, apply are 1.341 -available as parameterized antiquotations, e.g. @{map 4} for lists of 1.342 -quadruples. 1.343 - 1.344 -* Renamed "pairself" to "apply2", in accordance to @{apply 2}. 1.345 -INCOMPATIBILITY. 1.346 - 1.347 -* Synchronized.value (ML) is actually synchronized (as in Scala): 1.348 -subtle change of semantics with minimal potential for INCOMPATIBILITY. 1.349 - 1.350 * Goal.prove_multi is superseded by the fully general Goal.prove_common, 1.351 which also allows to specify a fork priority. 1.352 1.353 @@ -415,8 +416,16 @@ 1.354 1.355 *** System *** 1.356 1.357 -* Support for Proof General and Isar TTY loop has been discontinued. 1.358 -Minor INCOMPATIBILITY. 1.359 +* The Isabelle tool "update_cartouches" changes theory files to use 1.360 +cartouches instead of old-style {* verbatim *} or `alt_string` tokens. 1.361 + 1.362 +* The Isabelle tool "build" provides new options -k and -x. 1.363 + 1.364 +* Discontinued old-fashioned "codegen" tool. Code generation can always 1.365 +be externally triggered using an appropriate ROOT file plus a 1.366 +corresponding theory. Parametrization is possible using environment 1.367 +variables, or ML snippets in the most extreme cases. Minor 1.368 +INCOMPATIBILITY. 1.369 1.370 * JVM system property "isabelle.threads" determines size of Scala thread 1.371 pool, like Isabelle system option "threads" for ML. 1.372 @@ -425,22 +434,12 @@ 1.373 look-and-feel, via internal class name or symbolic name as in the jEdit 1.374 menu Global Options / Appearance. 1.375 1.376 -* System option "pretty_margin" is superseded by "thy_output_margin", 1.377 -which is also accessible via document antiquotation option "margin". 1.378 -Only the margin for document output may be changed, but not the global 1.379 -pretty printing: that is 76 for plain console output, and adapted 1.380 -dynamically in GUI front-ends. Implementations of document 1.381 -antiquotations need to observe the margin explicitly according to 1.382 -Thy_Output.string_of_margin. Minor INCOMPATIBILITY. 1.383 - 1.384 * Historical command-line terminator ";" is no longer accepted. Minor 1.385 INCOMPATIBILITY, use "isabelle update_semicolons" to remove obsolete 1.386 semicolons from theory sources. 1.387 1.388 -* The Isabelle tool "update_cartouches" changes theory files to use 1.389 -cartouches instead of old-style {* verbatim *} or `alt_string` tokens. 1.390 - 1.391 -* The Isabelle tool "build" provides new options -k and -x. 1.392 +* Support for Proof General and Isar TTY loop has been discontinued. 1.393 +Minor INCOMPATIBILITY. 1.394 1.395 1.396