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)