misc tuning for release;
authorwenzelm
Fri Jul 04 14:52:05 2014 +0200 (2014-07-04)
changeset 575045cf245c62c4c
parent 57503 3e04e25a751e
child 57505 63e2163c4736
misc tuning for release;
ANNOUNCE
NEWS
     1.1 --- a/ANNOUNCE	Fri Jul 04 11:39:34 2014 +0200
     1.2 +++ b/ANNOUNCE	Fri Jul 04 14:52:05 2014 +0200
     1.3 @@ -9,7 +9,8 @@
     1.4  * Improved Isabelle/jEdit Prover IDE: navigation, completion,
     1.5    spell-checking, Query panel, Simplifier Trace panel.
     1.6  
     1.7 -* Support for auxiliary files within the Prover IDE.
     1.8 +* Support for auxiliary files within the Prover IDE, notably
     1.9 +  Isabelle/ML.
    1.10  
    1.11  * Support for official Standard ML within the Prover IDE,
    1.12    independently of Isabelle theory and proof development.
    1.13 @@ -19,19 +20,19 @@
    1.14  
    1.15  * HOL tool enhancements: Nitpick, Sledgehammer.
    1.16  
    1.17 -* HOL: numerous library enhancements: Main, HOL-Multivariate_Analysis,
    1.18 -  HOL-Probability.
    1.19 -
    1.20  * HOL: internal SAT solver "cdclite" with models and proof traces.
    1.21  
    1.22  * HOL: updated SMT module, with support for SMT-LIB 2 and recent
    1.23    versions of Z3, as well as CVC3, CVC4.
    1.24  
    1.25 +* HOL: numerous library enhancements: Main, HOL-Multivariate_Analysis,
    1.26 +  HOL-Probability.
    1.27 +
    1.28 +* System integration: improved support of LateX on Windows platform.
    1.29 +
    1.30  * Updated and extended manuals: codegen, datatypes, implementation,
    1.31    isar-ref, jedit, system.
    1.32  
    1.33 -* System integration: improved support of LateX on Windows platform.
    1.34 -
    1.35  
    1.36  You may get Isabelle2013-2 from the following mirror sites:
    1.37  
     2.1 --- a/NEWS	Fri Jul 04 11:39:34 2014 +0200
     2.2 +++ b/NEWS	Fri Jul 04 14:52:05 2014 +0200
     2.3 @@ -15,6 +15,16 @@
     2.4  separate environments.  See also ~~/src/Tools/SML/Examples.thy for
     2.5  some examples.
     2.6  
     2.7 +* Standard tactics and proof methods such as "clarsimp", "auto" and
     2.8 +"safe" now preserve equality hypotheses "x = expr" where x is a free
     2.9 +variable.  Locale assumptions and chained facts containing "x"
    2.10 +continue to be useful.  The new method "hypsubst_thin" and the
    2.11 +configuration option "hypsubst_thin" (within the attribute name space)
    2.12 +restore the previous behavior.  INCOMPATIBILITY, especially where
    2.13 +induction is done after these methods or when the names of free and
    2.14 +bound variables clash.  As first approximation, old proofs may be
    2.15 +repaired by "using [[hypsubst_thin = true]]" in the critical spot.
    2.16 +
    2.17  * More static checking of proof methods, which allows the system to
    2.18  form a closure over the concrete syntax.  Method arguments should be
    2.19  processed in the original proof context as far as possible, before
    2.20 @@ -51,18 +61,6 @@
    2.21  * Updated and extended manuals: codegen, datatypes, implementation,
    2.22  isar-ref, jedit, system.
    2.23  
    2.24 -* Standard tactics and proof methods such as "clarsimp", "auto" and
    2.25 -"safe" now preserve equality hypotheses "x = expr" where x is a free
    2.26 -variable.  Locale assumptions and chained facts containing "x"
    2.27 -continue to be useful.  The new method "hypsubst_thin" and the
    2.28 -configuration option "hypsubst_thin" (within the attribute name space)
    2.29 -restore the previous behavior.
    2.30 -
    2.31 -INCOMPATIBILITY, especially where induction is done after these
    2.32 -methods or when the names of free and bound variables clash.  As first
    2.33 -approximation, old proofs may be repaired by "using [[hypsubst_thin =
    2.34 -true]]" in the critical spot.
    2.35 -
    2.36  
    2.37  *** Prover IDE -- Isabelle/Scala/jEdit ***
    2.38  
    2.39 @@ -122,37 +120,8 @@
    2.40  within the context.
    2.41  
    2.42  
    2.43 -
    2.44  *** Pure ***
    2.45  
    2.46 -* Basic constants of Pure use more conventional names and are always
    2.47 -qualified.  Rare INCOMPATIBILITY, but with potentially serious
    2.48 -consequences, notably for tools in Isabelle/ML.  The following
    2.49 -renaming needs to be applied:
    2.50 -
    2.51 -  ==             ~>  Pure.eq
    2.52 -  ==>            ~>  Pure.imp
    2.53 -  all            ~>  Pure.all
    2.54 -  TYPE           ~>  Pure.type
    2.55 -  dummy_pattern  ~>  Pure.dummy_pattern
    2.56 -
    2.57 -Systematic porting works by using the following theory setup on a
    2.58 -*previous* Isabelle version to introduce the new name accesses for the
    2.59 -old constants:
    2.60 -
    2.61 -setup {*
    2.62 -  fn thy => thy
    2.63 -    |> Sign.root_path
    2.64 -    |> Sign.const_alias (Binding.qualify true "Pure" @{binding eq}) "=="
    2.65 -    |> Sign.const_alias (Binding.qualify true "Pure" @{binding imp}) "==>"
    2.66 -    |> Sign.const_alias (Binding.qualify true "Pure" @{binding all}) "all"
    2.67 -    |> Sign.restore_naming thy
    2.68 -*}
    2.69 -
    2.70 -Thus ML antiquotations like @{const_name Pure.eq} may be used already.
    2.71 -Later the application is moved to the current Isabelle version, and
    2.72 -the auxiliary aliases are deleted.
    2.73 -
    2.74  * Low-level type-class commands 'classes', 'classrel', 'arities' have
    2.75  been discontinued to avoid the danger of non-trivial axiomatization
    2.76  that is not immediately visible.  INCOMPATIBILITY, use regular
    2.77 @@ -163,6 +132,34 @@
    2.78  Axclass.class_axiomatization, Axclass.classrel_axiomatization,
    2.79  Axclass.arity_axiomatization.
    2.80  
    2.81 +* Basic constants of Pure use more conventional names and are always
    2.82 +qualified.  Rare INCOMPATIBILITY, but with potentially serious
    2.83 +consequences, notably for tools in Isabelle/ML.  The following
    2.84 +renaming needs to be applied:
    2.85 +
    2.86 +  ==             ~>  Pure.eq
    2.87 +  ==>            ~>  Pure.imp
    2.88 +  all            ~>  Pure.all
    2.89 +  TYPE           ~>  Pure.type
    2.90 +  dummy_pattern  ~>  Pure.dummy_pattern
    2.91 +
    2.92 +Systematic porting works by using the following theory setup on a
    2.93 +*previous* Isabelle version to introduce the new name accesses for the
    2.94 +old constants:
    2.95 +
    2.96 +setup {*
    2.97 +  fn thy => thy
    2.98 +    |> Sign.root_path
    2.99 +    |> Sign.const_alias (Binding.qualify true "Pure" @{binding eq}) "=="
   2.100 +    |> Sign.const_alias (Binding.qualify true "Pure" @{binding imp}) "==>"
   2.101 +    |> Sign.const_alias (Binding.qualify true "Pure" @{binding all}) "all"
   2.102 +    |> Sign.restore_naming thy
   2.103 +*}
   2.104 +
   2.105 +Thus ML antiquotations like @{const_name Pure.eq} may be used already.
   2.106 +Later the application is moved to the current Isabelle version, and
   2.107 +the auxiliary aliases are deleted.
   2.108 +
   2.109  * Attributes "where" and "of" allow an optional context of local
   2.110  variables ('for' declaration): these variables become schematic in the
   2.111  instantiated theorem.
   2.112 @@ -186,22 +183,45 @@
   2.113  (only makes sense in practice, if outer syntax is delimited
   2.114  differently, e.g. via cartouches).
   2.115  
   2.116 +* Command 'print_term_bindings' supersedes 'print_binds' for clarity,
   2.117 +but the latter is retained some time as Proof General legacy.
   2.118 +
   2.119  * Code generator preprocessor: explicit control of simp tracing on a
   2.120  per-constant basis.  See attribute "code_preproc".
   2.121  
   2.122 -* Command 'print_term_bindings' supersedes 'print_binds' for clarity,
   2.123 -but the latter is retained some time as Proof General legacy.
   2.124 -
   2.125  
   2.126  *** HOL ***
   2.127  
   2.128 -* Qualified String.implode and String.explode.  INCOMPATIBILITY.
   2.129 +* Code generator: enforce case of identifiers only for strict target
   2.130 +language requirements.  INCOMPATIBILITY.
   2.131 +
   2.132 +* Code generator: explicit proof contexts in many ML interfaces.
   2.133 +INCOMPATIBILITY.
   2.134 +
   2.135 +* Code generator: minimize exported identifiers by default.  Minor
   2.136 +INCOMPATIBILITY.
   2.137 +
   2.138 +* Code generation for SML and OCaml: dropped arcane "no_signatures"
   2.139 +option.  Minor INCOMPATIBILITY.
   2.140 +
   2.141 +* "declare [[code abort: ...]]" replaces "code_abort ...".
   2.142 +INCOMPATIBILITY.
   2.143 +
   2.144 +* "declare [[code drop: ...]]" drops all code equations associated
   2.145 +with the given constants.
   2.146 +
   2.147 +* Code generations are provided for make, fields, extend and truncate
   2.148 +operations on records.
   2.149  
   2.150  * Command and antiquotation "value" are now hardcoded against nbe and
   2.151  ML.  Minor INCOMPATIBILITY.
   2.152  
   2.153 -* Separate command "approximate" for approximative computation in
   2.154 -src/HOL/Decision_Procs/Approximation.  Minor INCOMPATIBILITY.
   2.155 +* Renamed command 'enriched_type' to 'functor'. INCOMPATIBILITY.
   2.156 +
   2.157 +* The symbol "\<newline>" may be used within char or string literals
   2.158 +to represent (Char Nibble0 NibbleA), i.e. ASCII newline.
   2.159 +
   2.160 +* Qualified String.implode and String.explode.  INCOMPATIBILITY.
   2.161  
   2.162  * Adjustion of INF and SUP operations:
   2.163    - Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
   2.164 @@ -217,13 +237,6 @@
   2.165  
   2.166  INCOMPATIBILITY.
   2.167  
   2.168 -* Revisions to HOL/Number_Theory
   2.169 -  - consolidated the proofs of the binomial theorem
   2.170 -  - the function fib is again of type nat=>nat and not overloaded
   2.171 -  - no more references to Old_Number_Theory in the HOL libraries (except the AFP)
   2.172 -
   2.173 -INCOMPATIBILITY.
   2.174 -
   2.175  * Swapped orientation of facts image_comp and vimage_comp:
   2.176  
   2.177    image_compose ~> image_comp [symmetric]
   2.178 @@ -239,25 +252,6 @@
   2.179  [[simp_legacy_precond]].  This configuration option will disappear
   2.180  again in the future.  INCOMPATIBILITY.
   2.181  
   2.182 -* HOL-Word:
   2.183 -  - Abandoned fact collection "word_arith_alts", which is a duplicate
   2.184 -    of "word_arith_wis".
   2.185 -  - Dropped first (duplicated) element in fact collections
   2.186 -    "sint_word_ariths", "word_arith_alts", "uint_word_ariths",
   2.187 -    "uint_word_arith_bintrs".
   2.188 -
   2.189 -* Code generator: enforce case of identifiers only for strict target
   2.190 -language requirements.  INCOMPATIBILITY.
   2.191 -
   2.192 -* Code generator: explicit proof contexts in many ML interfaces.
   2.193 -INCOMPATIBILITY.
   2.194 -
   2.195 -* Code generator: minimize exported identifiers by default.  Minor
   2.196 -INCOMPATIBILITY.
   2.197 -
   2.198 -* Code generation for SML and OCaml: dropped arcane "no_signatures"
   2.199 -option.  Minor INCOMPATIBILITY.
   2.200 -
   2.201  * Simproc "finite_Collect" is no longer enabled by default, due to
   2.202  spurious crashes and other surprises.  Potential INCOMPATIBILITY.
   2.203  
   2.204 @@ -374,12 +368,8 @@
   2.205  
   2.206  INCOMPATIBILITY.
   2.207  
   2.208 -* New theory src/HOL/Cardinals/Ordinal_Arithmetic.thy.
   2.209 -
   2.210 -* New theory src/HOL/Library/Tree.thy.
   2.211 -
   2.212 -* Theory reorganization:
   2.213 -  Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy
   2.214 +* Theory reorganization: split of Big_Operators.thy into
   2.215 +Groups_Big.thy and Lattices_Big.thy.
   2.216  
   2.217  * Consolidated some facts about big group operators:
   2.218  
   2.219 @@ -486,22 +476,11 @@
   2.220  
   2.221  * Try0: Added 'algebra' and 'meson' to the set of proof methods.
   2.222  
   2.223 -* Command renaming: enriched_type ~> functor. INCOMPATIBILITY.
   2.224 -
   2.225 -* The symbol "\<newline>" may be used within char or string literals
   2.226 -to represent (Char Nibble0 NibbleA), i.e. ASCII newline.
   2.227 -
   2.228  * Activation of Z3 now works via "z3_non_commercial" system option
   2.229  (without requiring restart), instead of former settings variable
   2.230  "Z3_NON_COMMERCIAL".  The option can be edited in Isabelle/jEdit menu
   2.231  Plugin Options / Isabelle / General.
   2.232  
   2.233 -* "declare [[code abort: ...]]" replaces "code_abort ...".
   2.234 -INCOMPATIBILITY.
   2.235 -
   2.236 -* "declare [[code drop: ...]]" drops all code equations associated
   2.237 -with the given constants.
   2.238 -
   2.239  * Abolished slightly odd global lattice interpretation for min/max.
   2.240  
   2.241    Fact consolidations:
   2.242 @@ -557,15 +536,9 @@
   2.243  
   2.244  INCOMPATBILITY.
   2.245  
   2.246 -* HOL-Word: bit representations prefer type bool over type bit.
   2.247 -INCOMPATIBILITY.
   2.248 -
   2.249  * Theorem disambiguation Inf_le_Sup (on finite sets) ~>
   2.250  Inf_fin_le_Sup_fin.  INCOMPATIBILITY.
   2.251  
   2.252 -* Code generations are provided for make, fields, extend and truncate
   2.253 -operations on records.
   2.254 -
   2.255  * Qualified constant names Wellfounded.acc, Wellfounded.accp.
   2.256  INCOMPATIBILITY.
   2.257  
   2.258 @@ -633,9 +606,6 @@
   2.259  
   2.260  * SUP and INF generalized to conditionally_complete_lattice.
   2.261  
   2.262 -* Theory Lubs moved HOL image to HOL-Library. It is replaced by
   2.263 -Conditionally_Complete_Lattices.  INCOMPATIBILITY.
   2.264 -
   2.265  * Introduce bdd_above and bdd_below in theory
   2.266  Conditionally_Complete_Lattices, use them instead of explicitly
   2.267  stating boundedness of sets.
   2.268 @@ -764,6 +734,34 @@
   2.269    - Renamed "show_datatypes" to "show_types" and "hide_datatypes" to
   2.270      "hide_types".
   2.271  
   2.272 +* Theory Lubs moved HOL image to HOL-Library. It is replaced by
   2.273 +Conditionally_Complete_Lattices.  INCOMPATIBILITY.
   2.274 +
   2.275 +* HOL-Library: new theory src/HOL/Library/Tree.thy.
   2.276 +
   2.277 +* HOL-Library: removed theory src/HOL/Library/Kleene_Algebra.thy; it
   2.278 +is subsumed by session Kleene_Algebra in AFP.
   2.279 +
   2.280 +* HOL-Cardinals: new theory src/HOL/Cardinals/Ordinal_Arithmetic.thy.
   2.281 +
   2.282 +* HOL-Word: bit representations prefer type bool over type bit.
   2.283 +INCOMPATIBILITY.
   2.284 +
   2.285 +* HOL-Word:
   2.286 +  - Abandoned fact collection "word_arith_alts", which is a duplicate
   2.287 +    of "word_arith_wis".
   2.288 +  - Dropped first (duplicated) element in fact collections
   2.289 +    "sint_word_ariths", "word_arith_alts", "uint_word_ariths",
   2.290 +    "uint_word_arith_bintrs".
   2.291 +
   2.292 +* HOL-Number_Theory:
   2.293 +  - consolidated the proofs of the binomial theorem
   2.294 +  - the function fib is again of type nat => nat and not overloaded
   2.295 +  - no more references to Old_Number_Theory in the HOL libraries
   2.296 +    (except the AFP)
   2.297 +
   2.298 +INCOMPATIBILITY.
   2.299 +
   2.300  * HOL-Multivariate_Analysis:
   2.301    - Type class ordered_real_vector for ordered vector spaces.
   2.302    - New theory Complex_Basic_Analysis defining complex derivatives,
   2.303 @@ -908,8 +906,9 @@
   2.304    - Formalized properties about exponentially, Erlang, and normal
   2.305      distributed random variables.
   2.306  
   2.307 -* Removed theory src/HOL/Library/Kleene_Algebra.thy; it is subsumed by
   2.308 -session Kleene_Algebra in AFP.
   2.309 +* HOL-Decision_Procs: Separate command 'approximate' for approximative
   2.310 +computation in src/HOL/Decision_Procs/Approximation.  Minor
   2.311 +INCOMPATIBILITY.
   2.312  
   2.313  
   2.314  *** Scala ***
   2.315 @@ -926,20 +925,17 @@
   2.316  
   2.317  *** ML ***
   2.318  
   2.319 -* Moved ML_Compiler.exn_trace and other operations on exceptions to
   2.320 -structure Runtime.  Minor INCOMPATIBILITY.
   2.321 -
   2.322 -* Discontinued old Toplevel.debug in favour of system option
   2.323 -"ML_exception_trace", which may be also declared within the context
   2.324 -via "declare [[ML_exception_trace = true]]".  Minor INCOMPATIBILITY.
   2.325 -
   2.326 -* Renamed configuration option "ML_trace" to "ML_source_trace". Minor
   2.327 -INCOMPATIBILITY.
   2.328 -
   2.329 -* Configuration option "ML_print_depth" controls the pretty-printing
   2.330 -depth of the ML compiler within the context.  The old print_depth in
   2.331 -ML is still available as default_print_depth, but rarely used.  Minor
   2.332 -INCOMPATIBILITY.
   2.333 +* Subtle change of semantics of Thm.eq_thm: theory stamps are not
   2.334 +compared (according to Thm.thm_ord), but assumed to be covered by the
   2.335 +current background theory.  Thus equivalent data produced in different
   2.336 +branches of the theory graph usually coincides (e.g. relevant for
   2.337 +theory merge).  Note that the softer Thm.eq_thm_prop is often more
   2.338 +appropriate than Thm.eq_thm.
   2.339 +
   2.340 +* Proper context for basic Simplifier operations: rewrite_rule,
   2.341 +rewrite_goals_rule, rewrite_goals_tac etc. INCOMPATIBILITY, need to
   2.342 +pass runtime Proof.context (and ensure that the simplified entity
   2.343 +actually belongs to it).
   2.344  
   2.345  * Proper context discipline for read_instantiate and instantiate_tac:
   2.346  variables that are meant to become schematic need to be given as
   2.347 @@ -948,23 +944,26 @@
   2.348  declaration.  INCOMPATIBILITY, also due to potential change of indices
   2.349  of schematic variables.
   2.350  
   2.351 +* Moved ML_Compiler.exn_trace and other operations on exceptions to
   2.352 +structure Runtime.  Minor INCOMPATIBILITY.
   2.353 +
   2.354 +* Discontinued old Toplevel.debug in favour of system option
   2.355 +"ML_exception_trace", which may be also declared within the context
   2.356 +via "declare [[ML_exception_trace = true]]".  Minor INCOMPATIBILITY.
   2.357 +
   2.358 +* Renamed configuration option "ML_trace" to "ML_source_trace". Minor
   2.359 +INCOMPATIBILITY.
   2.360 +
   2.361 +* Configuration option "ML_print_depth" controls the pretty-printing
   2.362 +depth of the ML compiler within the context.  The old print_depth in
   2.363 +ML is still available as default_print_depth, but rarely used.  Minor
   2.364 +INCOMPATIBILITY.
   2.365 +
   2.366  * Toplevel function "use" refers to raw ML bootstrap environment,
   2.367  without Isar context nor antiquotations.  Potential INCOMPATIBILITY.
   2.368  Note that 'ML_file' is the canonical command to load ML files into the
   2.369  formal context.
   2.370  
   2.371 -* Proper context for basic Simplifier operations: rewrite_rule,
   2.372 -rewrite_goals_rule, rewrite_goals_tac etc. INCOMPATIBILITY, need to
   2.373 -pass runtime Proof.context (and ensure that the simplified entity
   2.374 -actually belongs to it).
   2.375 -
   2.376 -* Subtle change of semantics of Thm.eq_thm: theory stamps are not
   2.377 -compared (according to Thm.thm_ord), but assumed to be covered by the
   2.378 -current background theory.  Thus equivalent data produced in different
   2.379 -branches of the theory graph usually coincides (e.g. relevant for
   2.380 -theory merge).  Note that the softer Thm.eq_thm_prop is often more
   2.381 -appropriate than Thm.eq_thm.
   2.382 -
   2.383  * Simplified programming interface to define ML antiquotations, see
   2.384  structure ML_Antiquotation.  Minor INCOMPATIBILITY.
   2.385  
   2.386 @@ -985,17 +984,17 @@
   2.387  *** System ***
   2.388  
   2.389  * Proof General with its traditional helper scripts is now an optional
   2.390 -Isabelle component, e.g. ProofGeneral-4.2-2 from the Isabelle
   2.391 -component repository http://isabelle.in.tum.de/components/.  See also
   2.392 -the "system" manual for general explanations about add-on components,
   2.393 -notably those that are not bundled with the normal release.
   2.394 +Isabelle component, e.g. see ProofGeneral-4.2-2 from the Isabelle
   2.395 +component repository http://isabelle.in.tum.de/components/.  Note that
   2.396 +the "system" manual provides general explanations about add-on
   2.397 +components, especially those that are not bundled with the release.
   2.398  
   2.399  * The raw Isabelle process executable has been renamed from
   2.400  "isabelle-process" to "isabelle_process", which conforms to common
   2.401  shell naming conventions, and allows to define a shell function within
   2.402  the Isabelle environment to avoid dynamic path lookup.  Rare
   2.403 -incompatibility for old tools that do not use the $ISABELLE_PROCESS
   2.404 -settings variable yet.
   2.405 +incompatibility for old tools that do not use the ISABELLE_PROCESS
   2.406 +settings variable.
   2.407  
   2.408  * Former "isabelle tty" has been superseded by "isabelle console",
   2.409  with implicit build like "isabelle jedit", and without the mostly
   2.410 @@ -1018,14 +1017,14 @@
   2.411  repeated invocation in PIDE front-end: re-use single file
   2.412  $ISABELLE_HOME_USER/tmp/drafts.pdf and corresponding views.
   2.413  
   2.414 -* Windows: support for regular TeX installation (e.g. MiKTeX) instead
   2.415 -of TeX Live from Cygwin.
   2.416 -
   2.417  * Session ROOT specifications require explicit 'document_files' for
   2.418  robust dependencies on LaTeX sources.  Only these explicitly given
   2.419  files are copied to the document output directory, before document
   2.420  processing is started.
   2.421  
   2.422 +* Windows: support for regular TeX installation (e.g. MiKTeX) instead
   2.423 +of TeX Live from Cygwin.
   2.424 +
   2.425  
   2.426  
   2.427  New in Isabelle2013-2 (December 2013)