NEWS
changeset 60009 bd1c342dbbce
parent 60006 fd9191f0d323
child 60010 5fe58ca9cf40
     1.1 --- a/NEWS	Sat Apr 11 12:24:51 2015 +0200
     1.2 +++ b/NEWS	Sat Apr 11 12:40:03 2015 +0200
     1.3 @@ -4,8 +4,8 @@
     1.4  (Note: Isabelle/jEdit shows a tree-view of this file in Sidekick.)
     1.5  
     1.6  
     1.7 -New in this Isabelle version
     1.8 -----------------------------
     1.9 +New in Isabelle2015 (May 2015)
    1.10 +------------------------------
    1.11  
    1.12  *** General ***
    1.13  
    1.14 @@ -57,9 +57,6 @@
    1.15  
    1.16  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.17  
    1.18 -* Old graph browser (Java/AWT 1.1) is superseded by improved graphview
    1.19 -panel, which also produces PDF output without external tools.
    1.20 -
    1.21  * Improved folding mode "isabelle" based on Isar syntax. Alternatively,
    1.22  the "sidekick" mode may be used for document structure.
    1.23  
    1.24 @@ -77,12 +74,12 @@
    1.25  * Less waste of vertical space via negative line spacing (see Global
    1.26  Options / Text Area).
    1.27  
    1.28 +* Old graph browser (Java/AWT 1.1) is superseded by improved graphview
    1.29 +panel, which also produces PDF output without external tools.
    1.30 +
    1.31  
    1.32  *** Document preparation ***
    1.33  
    1.34 -* Discontinued obsolete option "document_graph": session_graph.pdf is
    1.35 -produced unconditionally for HTML browser_info and PDF-LaTeX document.
    1.36 -
    1.37  * Document markup commands 'chapter', 'section', 'subsection',
    1.38  'subsubsection', 'text', 'txt', 'text_raw' work uniformly in any
    1.39  context, even before the initial 'theory' command. Obsolete proof
    1.40 @@ -92,6 +89,17 @@
    1.41  should be replaced by 'chapter', 'section' etc. (using "isabelle
    1.42  update_header"). Minor INCOMPATIBILITY.
    1.43  
    1.44 +* Official support for "tt" style variants, via \isatt{...} or
    1.45 +\begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or
    1.46 +verbatim environment of LaTeX is no longer used. This allows @{ML} etc.
    1.47 +as argument to other macros (such as footnotes).
    1.48 +
    1.49 +* Document antiquotation @{verbatim} prints ASCII text literally in "tt"
    1.50 +style.
    1.51 +
    1.52 +* Discontinued obsolete option "document_graph": session_graph.pdf is
    1.53 +produced unconditionally for HTML browser_info and PDF-LaTeX document.
    1.54 +
    1.55  * Diagnostic commands and document markup commands within a proof do not
    1.56  affect the command tag for output. Thus commands like 'thm' are subject
    1.57  to proof document structure, and no longer "stick out" accidentally.
    1.58 @@ -106,21 +114,9 @@
    1.59  antiquotations need to observe the margin explicitly according to
    1.60  Thy_Output.string_of_margin. Minor INCOMPATIBILITY.
    1.61  
    1.62 -* Official support for "tt" style variants, via \isatt{...} or
    1.63 -\begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or
    1.64 -verbatim environment of LaTeX is no longer used. This allows @{ML} etc.
    1.65 -as argument to other macros (such as footnotes).
    1.66 -
    1.67 -* Document antiquotation @{verbatim} prints ASCII text literally in "tt"
    1.68 -style.
    1.69 -
    1.70  
    1.71  *** Pure ***
    1.72  
    1.73 -* Explicit instantiation via attributes "where", "of", and proof methods
    1.74 -"rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns
    1.75 -("_") that stand for anonymous local variables.
    1.76 -
    1.77  * Proof methods with explicit instantiation ("rule_tac", "subgoal_tac"
    1.78  etc.) allow an optional context of local variables ('for' declaration):
    1.79  these variables become schematic in the instantiated theorem; this
    1.80 @@ -130,13 +126,17 @@
    1.81  declare rule_insts_schematic = true temporarily and update to use local
    1.82  variable declarations or dummy patterns instead.
    1.83  
    1.84 +* Explicit instantiation via attributes "where", "of", and proof methods
    1.85 +"rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns
    1.86 +("_") that stand for anonymous local variables.
    1.87 +
    1.88  * Generated schematic variables in standard format of exported facts are
    1.89  incremented to avoid material in the proof context. Rare
    1.90  INCOMPATIBILITY, explicit instantiation sometimes needs to refer to
    1.91  different index.
    1.92  
    1.93 -* Command "class_deps" takes optional sort arguments constraining
    1.94 -the search space.
    1.95 +* Command "class_deps" takes optional sort arguments to constrain then
    1.96 +resulting class hierarchy.
    1.97  
    1.98  * Lexical separation of signed and unsigend numerals: categories "num"
    1.99  and "float" are unsigend.  INCOMPATIBILITY: subtle change in precedence
   1.100 @@ -150,88 +150,6 @@
   1.101  
   1.102  *** HOL ***
   1.103  
   1.104 -* Given up separate type class no_zero_divisors in favour of fully
   1.105 -algebraic semiring_no_zero_divisors. INCOMPATIBILITY.
   1.106 -
   1.107 -* Class linordered_semidom really requires no zero divisors.
   1.108 -INCOMPATIBILITY.
   1.109 -
   1.110 -* Classes division_ring, field and linordered_field always demand
   1.111 -"inverse 0 = 0". Given up separate classes division_ring_inverse_zero,
   1.112 -field_inverse_zero and linordered_field_inverse_zero. INCOMPATIBILITY.
   1.113 -
   1.114 -* Type classes cancel_ab_semigroup_add / cancel_monoid_add specify
   1.115 -explicit additive inverse operation. INCOMPATIBILITY.
   1.116 -
   1.117 -* New proof method "rewrite" (in theory ~~/src/HOL/Library/Rewrite) for
   1.118 -single-step rewriting with subterm selection based on patterns.
   1.119 -
   1.120 -* The functions "sin" and "cos" are now defined for any
   1.121 -"'{real_normed_algebra_1,banach}" type, so in particular on "real" and
   1.122 -"complex" uniformly. Minor INCOMPATIBILITY: type constraints may be
   1.123 -needed.
   1.124 -
   1.125 -* New library of properties of the complex transcendental functions sin,
   1.126 -cos, tan, exp, Ln, Arctan, Arcsin, Arccos. Ported from HOL Light.
   1.127 -
   1.128 -* The factorial function, "fact", now has type "nat => 'a" (of a sort
   1.129 -that admits numeric types including nat, int, real and complex.
   1.130 -INCOMPATIBILITY: an expression such as "fact 3 = 6" may require a type
   1.131 -constraint, and the combination "real (fact k)" is likely to be
   1.132 -unsatisfactory. If a type conversion is still necessary, then use
   1.133 -"of_nat (fact k)" or "real_of_nat (fact k)".
   1.134 -
   1.135 -* Removed functions "natfloor" and "natceiling", use "nat o floor" and
   1.136 -"nat o ceiling" instead. A few of the lemmas have been retained and
   1.137 -adapted: in their names "natfloor"/"natceiling" has been replaced by
   1.138 -"nat_floor"/"nat_ceiling".
   1.139 -
   1.140 -* Qualified some duplicated fact names required for boostrapping the
   1.141 -type class hierarchy:
   1.142 -  ab_add_uminus_conv_diff ~> diff_conv_add_uminus
   1.143 -  field_inverse_zero ~> inverse_zero
   1.144 -  field_divide_inverse ~> divide_inverse
   1.145 -  field_inverse ~> left_inverse
   1.146 -Minor INCOMPATIBILITY.
   1.147 -
   1.148 -* Eliminated fact duplicates:
   1.149 -  mult_less_imp_less_right ~> mult_right_less_imp_less
   1.150 -  mult_less_imp_less_left ~> mult_left_less_imp_less
   1.151 -Minor INCOMPATIBILITY.
   1.152 -
   1.153 -* Fact consolidation: even_less_0_iff is subsumed by
   1.154 -double_add_less_zero_iff_single_add_less_zero (simp by default anyway).
   1.155 -
   1.156 -* Add NO_MATCH-simproc, allows to check for syntactic non-equality.
   1.157 -
   1.158 -* Generalized and consolidated some theorems concerning divsibility:
   1.159 -  dvd_reduce ~> dvd_add_triv_right_iff
   1.160 -  dvd_plus_eq_right ~> dvd_add_right_iff
   1.161 -  dvd_plus_eq_left ~> dvd_add_left_iff
   1.162 -Minor INCOMPATIBILITY.
   1.163 -
   1.164 -* "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _"
   1.165 -and part of theory Main.
   1.166 -  even_def ~> even_iff_mod_2_eq_zero
   1.167 -INCOMPATIBILITY.
   1.168 -
   1.169 -* Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1. Minor
   1.170 -INCOMPATIBILITY.
   1.171 -
   1.172 -* field_simps: Use NO_MATCH-simproc for distribution rules, to avoid
   1.173 -non-termination in case of distributing a division. With this change
   1.174 -field_simps is in some cases slightly less powerful, if it fails try to
   1.175 -add algebra_simps, or use divide_simps. Minor INCOMPATIBILITY.
   1.176 -
   1.177 -* Bootstrap of listsum as special case of abstract product over lists.
   1.178 -Fact rename:
   1.179 -    listsum_def ~> listsum.eq_foldr
   1.180 -INCOMPATIBILITY.
   1.181 -
   1.182 -* Command and antiquotation "value" provide different evaluation slots
   1.183 -(again), where the previous strategy (NBE after ML) serves as default.
   1.184 -Minor INCOMPATIBILITY.
   1.185 -
   1.186  * New (co)datatype package:
   1.187    - The 'datatype_new' command has been renamed 'datatype'. The old
   1.188      command of that name is now called 'old_datatype' and is provided
   1.189 @@ -288,8 +206,6 @@
   1.190        ~~/src/HOL/Datatype.thy ~> ~~/src/HOL/Library/Old_Datatype.thy
   1.191      INCOMPATIBILITY.
   1.192  
   1.193 -* Product over lists via constant "listprod".
   1.194 -
   1.195  * Nitpick:
   1.196    - Fixed soundness bug related to the strict and nonstrict subset
   1.197      operations.
   1.198 @@ -321,18 +237,95 @@
   1.199    - New option 'smt_statistics' to display statistics of the new 'smt'
   1.200      method, especially runtime statistics of Z3 proof reconstruction.
   1.201  
   1.202 -* List: renamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc.
   1.203 +* Command and antiquotation "value" provide different evaluation slots
   1.204 +(again), where the previous strategy (NBE after ML) serves as default.
   1.205 +Minor INCOMPATIBILITY.
   1.206 +
   1.207 +* Add NO_MATCH-simproc, allows to check for syntactic non-equality.
   1.208 +
   1.209 +* field_simps: Use NO_MATCH-simproc for distribution rules, to avoid
   1.210 +non-termination in case of distributing a division. With this change
   1.211 +field_simps is in some cases slightly less powerful, if it fails try to
   1.212 +add algebra_simps, or use divide_simps. Minor INCOMPATIBILITY.
   1.213 +
   1.214 +* Separate class no_zero_divisors has been given up in favour of fully
   1.215 +algebraic semiring_no_zero_divisors. INCOMPATIBILITY.
   1.216 +
   1.217 +* Class linordered_semidom really requires no zero divisors.
   1.218 +INCOMPATIBILITY.
   1.219 +
   1.220 +* Classes division_ring, field and linordered_field always demand
   1.221 +"inverse 0 = 0". Given up separate classes division_ring_inverse_zero,
   1.222 +field_inverse_zero and linordered_field_inverse_zero. INCOMPATIBILITY.
   1.223 +
   1.224 +* Classes cancel_ab_semigroup_add / cancel_monoid_add specify explicit
   1.225 +additive inverse operation. INCOMPATIBILITY.
   1.226 +
   1.227 +* The functions "sin" and "cos" are now defined for any type of sort
   1.228 +"{real_normed_algebra_1,banach}" type, so in particular on "real" and
   1.229 +"complex" uniformly. Minor INCOMPATIBILITY: type constraints may be
   1.230 +needed.
   1.231 +
   1.232 +* New library of properties of the complex transcendental functions sin,
   1.233 +cos, tan, exp, Ln, Arctan, Arcsin, Arccos. Ported from HOL Light.
   1.234 +
   1.235 +* The factorial function, "fact", now has type "nat => 'a" (of a sort
   1.236 +that admits numeric types including nat, int, real and complex.
   1.237 +INCOMPATIBILITY: an expression such as "fact 3 = 6" may require a type
   1.238 +constraint, and the combination "real (fact k)" is likely to be
   1.239 +unsatisfactory. If a type conversion is still necessary, then use
   1.240 +"of_nat (fact k)" or "real_of_nat (fact k)".
   1.241 +
   1.242 +* Removed functions "natfloor" and "natceiling", use "nat o floor" and
   1.243 +"nat o ceiling" instead. A few of the lemmas have been retained and
   1.244 +adapted: in their names "natfloor"/"natceiling" has been replaced by
   1.245 +"nat_floor"/"nat_ceiling".
   1.246 +
   1.247 +* Qualified some duplicated fact names required for boostrapping the
   1.248 +type class hierarchy:
   1.249 +  ab_add_uminus_conv_diff ~> diff_conv_add_uminus
   1.250 +  field_inverse_zero ~> inverse_zero
   1.251 +  field_divide_inverse ~> divide_inverse
   1.252 +  field_inverse ~> left_inverse
   1.253 +Minor INCOMPATIBILITY.
   1.254 +
   1.255 +* Eliminated fact duplicates:
   1.256 +  mult_less_imp_less_right ~> mult_right_less_imp_less
   1.257 +  mult_less_imp_less_left ~> mult_left_less_imp_less
   1.258 +Minor INCOMPATIBILITY.
   1.259 +
   1.260 +* Fact consolidation: even_less_0_iff is subsumed by
   1.261 +double_add_less_zero_iff_single_add_less_zero (simp by default anyway).
   1.262 +
   1.263 +* Generalized and consolidated some theorems concerning divsibility:
   1.264 +  dvd_reduce ~> dvd_add_triv_right_iff
   1.265 +  dvd_plus_eq_right ~> dvd_add_right_iff
   1.266 +  dvd_plus_eq_left ~> dvd_add_left_iff
   1.267 +Minor INCOMPATIBILITY.
   1.268 +
   1.269 +* "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _"
   1.270 +and part of theory Main.
   1.271 +  even_def ~> even_iff_mod_2_eq_zero
   1.272 +INCOMPATIBILITY.
   1.273 +
   1.274 +* Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1. Minor
   1.275 +INCOMPATIBILITY.
   1.276 +
   1.277 +* Bootstrap of listsum as special case of abstract product over lists.
   1.278 +Fact rename:
   1.279 +    listsum_def ~> listsum.eq_foldr
   1.280 +INCOMPATIBILITY.
   1.281 +
   1.282 +* Product over lists via constant "listprod".
   1.283 +
   1.284 +* Theory List: renamed drop_Suc_conv_tl and nth_drop' to
   1.285 +Cons_nth_drop_Suc.
   1.286  
   1.287  * New infrastructure for compiling, running, evaluating and testing
   1.288  generated code in target languages in HOL/Library/Code_Test. See
   1.289  HOL/Codegenerator_Test/Code_Test* for examples.
   1.290  
   1.291 -* Library/Sum_of_Squares: simplified and improved "sos" method. Always
   1.292 -use local CSDP executable, which is much faster than the NEOS server.
   1.293 -The "sos_cert" functionality is invoked as "sos" with additional
   1.294 -argument. Minor INCOMPATIBILITY.
   1.295 -
   1.296 -* Theory "Library/Multiset":
   1.297 +* Library/Multiset:
   1.298    - Introduced "replicate_mset" operation.
   1.299    - Introduced alternative characterizations of the multiset ordering in
   1.300      "Library/Multiset_Order".
   1.301 @@ -363,14 +356,17 @@
   1.302        in_Union_mset_iff [iff]
   1.303      INCOMPATIBILITY.
   1.304  
   1.305 -* HOL-Decision_Procs:
   1.306 -  - New counterexample generator quickcheck[approximation] for
   1.307 -    inequalities of transcendental functions.
   1.308 -    Uses hardware floating point arithmetic to randomly discover
   1.309 -    potential counterexamples. Counterexamples are certified with the
   1.310 -    'approximation' method.
   1.311 -    See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for
   1.312 -    examples.
   1.313 +* Library/Sum_of_Squares: simplified and improved "sos" method. Always
   1.314 +use local CSDP executable, which is much faster than the NEOS server.
   1.315 +The "sos_cert" functionality is invoked as "sos" with additional
   1.316 +argument. Minor INCOMPATIBILITY.
   1.317 +
   1.318 +* HOL-Decision_Procs: New counterexample generator quickcheck
   1.319 +[approximation] for inequalities of transcendental functions. Uses
   1.320 +hardware floating point arithmetic to randomly discover potential
   1.321 +counterexamples. Counterexamples are certified with the 'approximation'
   1.322 +method. See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for
   1.323 +examples.
   1.324  
   1.325  * HOL-Probability: Reworked measurability prover
   1.326    - applies destructor rules repeatetly
   1.327 @@ -378,11 +374,19 @@
   1.328    - added congruence rules to rewrite measure spaces under the sets
   1.329      projection
   1.330  
   1.331 +* New proof method "rewrite" (in theory ~~/src/HOL/Library/Rewrite) for
   1.332 +single-step rewriting with subterm selection based on patterns.
   1.333 +
   1.334  
   1.335  *** ML ***
   1.336  
   1.337 -* Cartouches within ML sources are turned into values of type
   1.338 -Input.source (with formal position information).
   1.339 +* Subtle change of name space policy: undeclared entries are now
   1.340 +considered inaccessible, instead of accessible via the fully-qualified
   1.341 +internal name. This mainly affects Name_Space.intern (and derivatives),
   1.342 +which may produce an unexpected Long_Name.hidden prefix. Note that
   1.343 +contempory applications use the strict Name_Space.check (and
   1.344 +derivatives) instead, which is not affected by the change. Potential
   1.345 +INCOMPATIBILITY in rare applications of Name_Space.intern.
   1.346  
   1.347  * Basic combinators map, fold, fold_map, split_list, apply are available
   1.348  as parameterized antiquotations, e.g. @{map 4} for lists of quadruples.
   1.349 @@ -397,8 +401,8 @@
   1.350  INCOMPATIBILITY: synchronized access needs to be atomic and cannot be
   1.351  nested.
   1.352  
   1.353 -* Synchronized.value (ML) is actually synchronized (as in Scala):
   1.354 -subtle change of semantics with minimal potential for INCOMPATIBILITY.
   1.355 +* Synchronized.value (ML) is actually synchronized (as in Scala): subtle
   1.356 +change of semantics with minimal potential for INCOMPATIBILITY.
   1.357  
   1.358  * The main operations to certify logical entities are Thm.ctyp_of and
   1.359  Thm.cterm_of with a local context; old-style global theory variants are
   1.360 @@ -409,14 +413,6 @@
   1.361  INCOMPATIBILITY, need to use qualified Thm.prop_of, Thm.cterm_of,
   1.362  Thm.term_of etc.
   1.363  
   1.364 -* Subtle change of name space policy: undeclared entries are now
   1.365 -considered inaccessible, instead of accessible via the fully-qualified
   1.366 -internal name. This mainly affects Name_Space.intern (and derivatives),
   1.367 -which may produce an unexpected Long_Name.hidden prefix. Note that
   1.368 -contempory applications use the strict Name_Space.check (and
   1.369 -derivatives) instead, which is not affected by the change. Potential
   1.370 -INCOMPATIBILITY in rare applications of Name_Space.intern.
   1.371 -
   1.372  * Proper context for various elementary tactics: assume_tac,
   1.373  resolve_tac, eresolve_tac, dresolve_tac, forward_tac, match_tac,
   1.374  compose_tac, Splitter.split_tac etc. INCOMPATIBILITY.
   1.375 @@ -431,6 +427,9 @@
   1.376  @{command_keyword COMMAND} (usually without quotes and with PIDE
   1.377  markup). Minor INCOMPATIBILITY.
   1.378  
   1.379 +* Cartouches within ML sources are turned into values of type
   1.380 +Input.source (with formal position information).
   1.381 +
   1.382  
   1.383  *** System ***
   1.384  
   1.385 @@ -457,7 +456,7 @@
   1.386  semicolons from theory sources.
   1.387  
   1.388  * Support for Proof General and Isar TTY loop has been discontinued.
   1.389 -Minor INCOMPATIBILITY.
   1.390 +Minor INCOMPATIBILITY, use standard PIDE infrastructure instead.
   1.391  
   1.392  
   1.393