# HG changeset patch
# User wenzelm
# Date 1503327326 7200
# Node ID 1b7d66d62035f708046773c1444f361f912d7b69
# Parent 80736667cc2ee907c5f2ebc343684169fab86406
misc tuning and updates for release;
diff r 80736667cc2e r 1b7d66d62035 NEWS
 a/NEWS Mon Aug 21 16:12:52 2017 +0200
+++ b/NEWS Mon Aug 21 16:55:26 2017 +0200
@@ 4,8 +4,8 @@
(Note: Isabelle/jEdit shows a treeview of the NEWS file in Sidekick.)
New in this Isabelle version

+New in Isabelle2017 (October 2017)
+
*** General ***
@@ 29,17 +29,11 @@
In order to import theories from other sessions, the ROOT file format
provides a new 'sessions' keyword. In contrast, a theory that is
imported in the oldfashioned manner via an explicit filesystem path
belongs to the current session, and might cause theory name confusion
+belongs to the current session, and might cause theory name conflicts
later on. Theories that are imported from other sessions are excluded
from the current session document. The commandline tool "isabelle
imports" helps to update theory imports.
Properly qualified imports allow the Prover IDE to process arbitrary
theory hierarchies independently of the underlying logic session image
(e.g. option "isabelle jedit l"), but the directory structure needs to
be known in advance (e.g. option "isabelle jedit d" or a line in the
file $ISABELLE_HOME_USER/ROOTS).

* The main theory entry points for some nonHOL sessions have changed,
to avoid confusion with the global name "Main" of the session HOL. This
leads to the follow renamings:
@@ 52,6 +46,10 @@
INCOMPATIBILITY.
+* Commands 'alias' and 'type_alias' introduce aliases for constants and
+type constructors, respectively. This allows adhoc changes to namespace
+accesses within global or local theory contexts, e.g. within a 'bundle'.
+
* Document antiquotations @{prf} and @{full_prf} output proof terms
(again) in the same way as commands 'prf' and 'full_prf'.
@@ 70,24 +68,14 @@
src/HOL/Decision_Procs/Reflective_Field.thy for examples and the
tutorial on code generation.
* Commands 'alias' and 'type_alias' introduce aliases for constants and
type constructors, respectively. This allows adhoc changes to namespace
accesses within global or local theory contexts, e.g. within a 'bundle'.

*** Prover IDE  Isabelle/Scala/jEdit ***
* Automatic indentation is more careful to avoid redundant spaces in
intermediate situations. Keywords are indented after input (via typed
characters or completion); see also option "jedit_indent_input".

* Action "isabelle.preview" opens an HTML preview of the current theory
document in the default web browser.

* Commandline invocation "isabelle jedit R l SESSION" uses the parent
image of the SESSION, with qualified theory imports restricted to that
portion of the session graph. Moreover, the ROOT entry of the SESSION is
opened in the editor.
+* Sessionqualified theory imports allow the Prover IDE to process
+arbitrary theory hierarchies independently of the underlying logic
+session image (e.g. option "isabelle jedit l"), but the directory
+structure needs to be known in advance (e.g. option "isabelle jedit d"
+or a line in the file $ISABELLE_HOME_USER/ROOTS).
* The PIDE document model maintains file content independently of the
status of jEdit editor buffers. Reloading jEdit buffers no longer causes
@@ 105,122 +93,96 @@
painted with thick lines; remaining errors in this situation are
represented by a different border color.
+* Automatic indentation is more careful to avoid redundant spaces in
+intermediate situations. Keywords are indented after input (via typed
+characters or completion); see also option "jedit_indent_input".
+
+* Action "isabelle.preview" opens an HTML preview of the current theory
+document in the default web browser.
+
+* Commandline invocation "isabelle jedit R l SESSION" uses the parent
+image of the SESSION, with qualified theory imports restricted to that
+portion of the session graph. Moreover, the ROOT entry of the SESSION is
+opened in the editor.
+
* The main Isabelle/jEdit plugin may be restarted manually (using the
jEdit Plugin Manager), as long as the "Isabelle Base" plugin remains
enabled at all times.
* Update to jedit5.4.0.
+* Update to current jedit5.4.0.
*** Pure ***
* Deleting the last code equations for a particular function using
[code del] results in function with no equations (runtime abort) rather
than an unimplemented function (generation time abort). Use explicit
[[code drop:]] to enforce the latter. Minor INCOMPATIBILTIY.
+than an unimplemented function (generation time abort). Use explicit
+[[code drop:]] to enforce the latter. Minor INCOMPATIBILTIY.
* Proper concept of code declarations in code.ML:
  Regular code declarations act only on the global theory level,
 being ignored with warnings if syntactically malformed.
  Explicitly global code declarations yield errors if syntactically malformed.
  Default code declarations are silently ignored if syntactically malformed.
+  Regular code declarations act only on the global theory level, being
+ ignored with warnings if syntactically malformed.
+  Explicitly global code declarations yield errors if syntactically
+ malformed.
+  Default code declarations are silently ignored if syntactically
+ malformed.
Minor INCOMPATIBILITY.
* Clarified and standardized internal data bookkeeping of code declarations:
history of serials allows to track potentially nonmonotonous declarations
appropriately. Minor INCOMPATIBILITY.
+* Clarified and standardized internal data bookkeeping of code
+declarations: history of serials allows to track potentially
+nonmonotonous declarations appropriately. Minor INCOMPATIBILITY.
*** HOL ***
* Theory Library/Pattern_Aliases provides input syntax for pattern
aliases as known from Haskell, Scala and ML.

* Constant "subseq" in Topological_Spaces removed and subsumed by
"strict_mono". Some basic lemmas specific to "subseq" have been renamed
accordingly, e.g. "subseq_o" > "strict_mono_o" etc.
+* SMT module:
+  A new option, 'smt_nat_as_int', has been added to translate 'nat' to
+ 'int' and benefit from the SMT solver's theory reasoning. It is
+ disabled by default.
+  The legacy module "src/HOL/Library/Old_SMT.thy" has been removed.
+  Several small issues have been rectified in the 'smt' command.
+
+* (Co)datatype package: The 'size_gen_o_map' lemma is no longer
+generated for datatypes with type class annotations. As a result, the
+tactic that derives it no longer fails on nested datatypes. Slight
+INCOMPATIBILITY.
* Command and antiquotation "value" with modified default strategy:
terms without free variables are always evaluated using plain evaluation
only, with no fallback on normalization by evaluation.
Minor INCOMPATIBILITY.

* Notions of squarefreeness, nth powers, and prime powers in
HOLComputational_Algebra and HOLNumber_Theory.

* Material on infinite products in HOLAnalysis

* Theory List:
 "sublist" renamed to "nths" in analogy with "nth".
 "sublisteq" renamed to "subseq".
 Minor INCOMPATIBILITY.
 New generic function "sorted_wrt"
+only, with no fallback on normalization by evaluation. Minor
+INCOMPATIBILITY.
* Theories "GCD" and "Binomial" are already included in "Main" (instead
of "Complex_Main").
* Constants E/L/F in Library/Formal_Power_Series were renamed to
fps_exp/fps_ln/fps_hypergeo to avoid polluting the name space.
INCOMPATIBILITY.

* Theory Totient in session Number_Theory introduces basic notions
about Euler's totient function previously hidden as solitary example
in theory Residues. Definition changed so that "totient 1 = 1" in
agreement with the literature. Minor INCOMPATIBILITY.

* Session "Computional_Algebra" covers many previously scattered
theories, notably Euclidean_Algorithm, Factorial_Ring, Formal_Power_Series,
Fraction_Field, Fundamental_Theorem_Algebra, Normalized_Fraction,
Polynomial_FPS, Polynomial, Primes. Minor INCOMPATIBILITY.

* Constant "surj" is a full input/output abbreviation (again).
Minor INCOMPATIBILITY.
* Theory Library/FinFun has been moved to AFP (again). INCOMPATIBILITY.

* Some old and rarely used ASCII replacement syntax has been removed.
INCOMPATIBILITY, standard syntax with symbols should be used instead.
The subsequent commands help to reproduce the old forms, e.g. to
simplify porting old theories:

syntax (ASCII)
 "_PiE" :: "pttrn \ 'a set \ 'b set \ ('a \ 'b) set" ("(3PIE _:_./ _)" 10)
 "_Pi" :: "pttrn \ 'a set \ 'b set \ ('a \ 'b) set" ("(3PI _:_./ _)" 10)
 "_lam" :: "pttrn \ 'a set \ 'a \ 'b \ ('a \ 'b)" ("(3%_:_./ _)" [0,0,3] 3)

* Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively.
INCOMPATIBILITY.
* Renamed ii to imaginary_unit in order to free up ii as a variable name.
The syntax \ remains available.
INCOMPATIBILITY.

* Dropped abbreviations transP, antisymP, single_valuedP;
use constants transp, antisymp, single_valuedp instead.
INCOMPATIBILITY.

* Algebraic type class hierarchy of euclidean (semi)rings in HOL:
euclidean_(semi)ring, euclidean_(semi)ring_cancel,
unique_euclidean_(semi)ring; instantiation requires
provision of a euclidean size.

* Reworking of theory Euclidean_Algorithm in session HOLNumber_Theory:
  Euclidean induction is available as rule eucl_induct;
  Constants Euclidean_Algorithm.gcd, Euclidean_Algorithm.lcm,
 Euclidean_Algorithm.Gcd and Euclidean_Algorithm.Lcm allow
 easy instantiation of euclidean (semi)rings as GCD (semi)rings.
  Coefficients obtained by extended euclidean algorithm are
 available as "bezout_coefficients".
INCOMPATIBILITY.

* Named collection mod_simps covers various congruence rules
concerning mod, replacing former zmod_simps.
INCOMPATIBILITY.
+* Renamed ii to imaginary_unit in order to free up ii as a variable
+name. The syntax \ remains available. INCOMPATIBILITY.
+
+* Dropped abbreviations transP, antisymP, single_valuedP; use constants
+transp, antisymp, single_valuedp instead. INCOMPATIBILITY.
+
+* Constant "subseq" in Topological_Spaces has been removed  it is
+subsumed by "strict_mono". Some basic lemmas specific to "subseq" have
+been renamed accordingly, e.g. "subseq_o" > "strict_mono_o" etc.
+
+* Theory List: "sublist" renamed to "nths" in analogy with "nth", and
+"sublisteq" renamed to "subseq". Minor INCOMPATIBILITY.
+
+* Theory List: new generic function "sorted_wrt".
+
+* Named theorems mod_simps covers various congruence rules concerning
+mod, replacing former zmod_simps. INCOMPATIBILITY.
* Swapped orientation of congruence rules mod_add_left_eq,
mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,
mod_diff_eq. INCOMPATIBILITY.
+mod_diff_eq. INCOMPATIBILITY.
* Generalized some facts:
measure_induct_rule
@@ 231,45 +193,76 @@
zmod_eq_dvd_iff ~> mod_eq_dvd_iff
INCOMPATIBILITY.
* (Co)datatype package:
  The 'size_gen_o_map' lemma is no longer generated for datatypes
 with type class annotations. As a result, the tactic that derives
 it no longer fails on nested datatypes. Slight INCOMPATIBILITY.

* Session HOLAlgebra extended by additional lattice theory: the
KnasterTarski fixed point theorem and Galois Connections.

* SMT module:
  A new option, 'smt_nat_as_int', has been added to translate 'nat' to
 'int' and benefit from the SMT solver's theory reasoning. It is disabled
 by default.
  The legacy module 'src/HOL/Library/Old_SMT.thy' has been removed.
  Several small issues have been rectified in the 'smt' command.
+* Algebraic type class hierarchy of euclidean (semi)rings in HOL:
+euclidean_(semi)ring, euclidean_(semi)ring_cancel,
+unique_euclidean_(semi)ring; instantiation requires provision of a
+euclidean size.
+
+* Theory "HOLNumber_Theory.Euclidean_Algorithm" has been reworked:
+  Euclidean induction is available as rule eucl_induct.
+  Constants Euclidean_Algorithm.gcd, Euclidean_Algorithm.lcm,
+ Euclidean_Algorithm.Gcd and Euclidean_Algorithm.Lcm allow
+ easy instantiation of euclidean (semi)rings as GCD (semi)rings.
+  Coefficients obtained by extended euclidean algorithm are
+ available as "bezout_coefficients".
+INCOMPATIBILITY.
+
+* Theory "Number_Theory.Totient" introduces basic notions about Euler's
+totient function previously hidden as solitary example in theory
+Residues. Definition changed so that "totient 1 = 1" in agreement with
+the literature. Minor INCOMPATIBILITY.
+
+* Theory "HOLLibrary.Permutations": theorem bij_swap_ompose_bij has
+been renamed to bij_swap_compose_bij. INCOMPATIBILITY.
+
+* Theory "HOLLibrary.Formal_Power_Series": constants E/L/F have been
+renamed to fps_exp/fps_ln/fps_hypergeo to avoid polluting the name
+space. INCOMPATIBILITY.
+
+* Theory "HOLLibrary.FinFun" has been moved to AFP (again).
+INCOMPATIBILITY.
+
+* Theory "HOLLibrary.FuncSet": some old and rarely used ASCII
+replacement syntax has been removed. INCOMPATIBILITY, standard syntax
+with symbols should be used instead. The subsequent commands help to
+reproduce the old forms, e.g. to simplify porting old theories:
+
+syntax (ASCII)
+ "_PiE" :: "pttrn \ 'a set \ 'b set \ ('a \ 'b) set" ("(3PIE _:_./ _)" 10)
+ "_Pi" :: "pttrn \ 'a set \ 'b set \ ('a \ 'b) set" ("(3PI _:_./ _)" 10)
+ "_lam" :: "pttrn \ 'a set \ 'a \ 'b \ ('a \ 'b)" ("(3%_:_./ _)" [0,0,3] 3)
+
+* Theory "HOLLibrary.Multiset": the simprocs on subsets operators of
+multisets have been renamed:
+
+ msetless_cancel_numerals ~> msetsubset_cancel
+ msetle_cancel_numerals ~> msetsubset_eq_cancel
+
+INCOMPATIBILITY.
+
+* Theory "HOLLibrary.Pattern_Aliases" provides input syntax for pattern
+aliases as known from Haskell, Scala and ML.
* Session HOLAnalysis: more material involving arcs, paths, covering
spaces, innessential maps, retracts. Major results include the Jordan
Curve Theorem and the Great Picard Theorem.

* The theorem in Permutations has been renamed:
 bij_swap_ompose_bij ~> bij_swap_compose_bij

* Session HOLLibrary: The simprocs on subsets operators of multisets
have been renamed:
 msetless_cancel_numerals ~> msetsubset_cancel
 msetle_cancel_numerals ~> msetsubset_eq_cancel
INCOMPATIBILITY.

* Session HOLLibrary: The suffix _numerals has been removed from the
name of the simprocs on multisets. INCOMPATIBILITY.
+spaces, innessential maps, retracts, material on infinite products.
+Major results include the Jordan Curve Theorem and the Great Picard
+Theorem.
+
+* Session HOLAlgebra has been extended by additional lattice theory:
+the KnasterTarski fixed point theorem and Galois Connections.
+
+* Sessions HOLComputational_Algebra and HOLNumber_Theory: new notions
+of squarefreeness, nth powers, and prime powers.
+
+* Session "HOLComputional_Algebra" covers many previously scattered
+theories, notably Euclidean_Algorithm, Factorial_Ring,
+Formal_Power_Series, Fraction_Field, Fundamental_Theorem_Algebra,
+Normalized_Fraction, Polynomial_FPS, Polynomial, Primes. Minor
+INCOMPATIBILITY.
*** System ***
* Option parallel_proofs is 1 by default (instead of more aggressive 2).
This requires less heap space and avoids burning parallel CPU cycles,
while full subproof parallelization is enabled for repeated builds
(according to parallel_subproofs_threshold).

* Prover IDE support for the Visual Studio Code editor and language
server protocol, via the "isabelle vscode_server" tool (see also
src/Tools/VSCode/README.md). The example application within the VS code
@@ 277,27 +270,24 @@
(the "Marketplace"). It serves as example for further potential IDE
frontends.
* ISABELLE_SCALA_BUILD_OPTIONS has been renamed to
ISABELLE_SCALAC_OPTIONS. Rare INCOMPATIBILITY.

* Isabelle settings ISABELLE_WINDOWS_PLATFORM,
ISABELLE_WINDOWS_PLATFORM32, ISABELLE_WINDOWS_PLATFORM64 indicate the
native Windows platform (independently of the Cygwin installation). This
is analogous to ISABELLE_PLATFORM, ISABELLE_PLATFORM32,
ISABELLE_PLATFORM64.
+* System option "parallel_proofs" is 1 by default (instead of more
+aggressive 2). This requires less heap space and avoids burning parallel
+CPU cycles, while full subproof parallelization is enabled for repeated
+builds (according to parallel_subproofs_threshold).
* System option "record_proofs" allows to change the global
Proofterm.proofs variable for a session. Regular values are are 0, 1, 2;
a negative value means the current state in the ML heap image remains
unchanged.
* Commandline tool "isabelle imports" helps to maintain theory imports
wrt. session structure. Examples:

 isabelle imports I a
 isabelle imports U a
 isabelle imports U i a
 isabelle imports M a d '~~/src/Benchmarks'
+* Isabelle settings variable ISABELLE_SCALA_BUILD_OPTIONS has been
+renamed to ISABELLE_SCALAC_OPTIONS. Rare INCOMPATIBILITY.
+
+* Isabelle settings variables ISABELLE_WINDOWS_PLATFORM,
+ISABELLE_WINDOWS_PLATFORM32, ISABELLE_WINDOWS_PLATFORM64 indicate the
+native Windows platform (independently of the Cygwin installation). This
+is analogous to ISABELLE_PLATFORM, ISABELLE_PLATFORM32,
+ISABELLE_PLATFORM64.
* Isabelle/Scala: the SQL module supports access to relational
databases, either as plain file (SQLite) or fullscale server
@@ 308,6 +298,14 @@
https://www.sqlite.org/appfileformat.html). This allows systematic
access via operations from module Sessions.Store in Isabelle/Scala.
+* Commandline tool "isabelle imports" helps to maintain theory imports
+wrt. session structure. Examples:
+
+ isabelle imports I a
+ isabelle imports U a
+ isabelle imports U i a
+ isabelle imports M a d '~~/src/Benchmarks'
+
New in Isabelle20161 (December 2016)
