misc tuning for release;
authorwenzelm
Wed Apr 08 11:13:53 2015 +0200 (2015-04-08)
changeset 599518c49daca5d9f
parent 59950 364b0512ce74
child 59952 550b74e9b08c
misc tuning for release;
NEWS
     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