misc tuning for release;
authorwenzelm
Sat Oct 01 12:03:27 2016 +0200 (2016-10-01)
changeset 63977ec0fb01c6d50
parent 63976 c1a481bb82d3
child 63978 efc958d2fe00
child 63979 95c3ae4baba8
misc tuning for release;
NEWS
     1.1 --- a/NEWS	Sat Oct 01 11:14:00 2016 +0200
     1.2 +++ b/NEWS	Sat Oct 01 12:03:27 2016 +0200
     1.3 @@ -9,41 +9,6 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 -* Embedded content (e.g. the inner syntax of types, terms, props) may be
     1.8 -delimited uniformly via cartouches. This works better than old-fashioned
     1.9 -quotes when sub-languages are nested.
    1.10 -
    1.11 -* Type-inference improves sorts of newly introduced type variables for
    1.12 -the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL).
    1.13 -Thus terms like "f x" or "\<And>x. P x" without any further syntactic context
    1.14 -produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare
    1.15 -INCOMPATIBILITY, need to provide explicit type constraints for Pure
    1.16 -types where this is really intended.
    1.17 -
    1.18 -* Simplified outer syntax: uniform category "name" includes long
    1.19 -identifiers. Former "xname" / "nameref" / "name reference" has been
    1.20 -discontinued.
    1.21 -
    1.22 -* Mixfix annotations support general block properties, with syntax
    1.23 -"(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent",
    1.24 -"unbreakable", "markup". The existing notation "(DIGITS" is equivalent
    1.25 -to "(\<open>indent=DIGITS\<close>". The former notation "(00" for unbreakable blocks
    1.26 -is superseded by "(\<open>unbreabable\<close>" --- rare INCOMPATIBILITY.
    1.27 -
    1.28 -* Mixfix annotations support delimiters like \<^control>\<open>cartouche\<close> --
    1.29 -this allows special forms of document output.
    1.30 -
    1.31 -* Raw LaTeX output now works via \<^latex>\<open>...\<close> instead of raw control
    1.32 -symbol \<^raw:...>. INCOMPATIBILITY, notably for LaTeXsugar.thy and its
    1.33 -derivatives.
    1.34 -
    1.35 -* \<^raw:...> symbols are no longer supported.
    1.36 -
    1.37 -* New symbol \<circle>, e.g. for temporal operator.
    1.38 -
    1.39 -* Old 'header' command is no longer supported (legacy since
    1.40 -Isabelle2015).
    1.41 -
    1.42  * Command 'bundle' provides a local theory target to define a bundle
    1.43  from the body of specification commands (such as 'declare',
    1.44  'declaration', 'notation', 'lemmas', 'lemma'). For example:
    1.45 @@ -58,48 +23,64 @@
    1.46  context. Unlike "context includes ... begin", the effect of 'unbundle'
    1.47  on the target context persists, until different declarations are given.
    1.48  
    1.49 -* Splitter in simp, auto and friends:
    1.50 -- The syntax "split add" has been discontinued, use plain "split".
    1.51 -- For situations with many conditional or case expressions,
    1.52 -there is an alternative splitting strategy that can be much faster.
    1.53 -It is selected by writing "split!" instead of "split". It applies
    1.54 -safe introduction and elimination rules after each split rule.
    1.55 -As a result the subgoal may be split into several subgoals.
    1.56 +* Simplified outer syntax: uniform category "name" includes long
    1.57 +identifiers. Former "xname" / "nameref" / "name reference" has been
    1.58 +discontinued.
    1.59 +
    1.60 +* Embedded content (e.g. the inner syntax of types, terms, props) may be
    1.61 +delimited uniformly via cartouches. This works better than old-fashioned
    1.62 +quotes when sub-languages are nested.
    1.63 +
    1.64 +* Mixfix annotations support general block properties, with syntax
    1.65 +"(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent",
    1.66 +"unbreakable", "markup". The existing notation "(DIGITS" is equivalent
    1.67 +to "(\<open>indent=DIGITS\<close>". The former notation "(00" for unbreakable blocks
    1.68 +is superseded by "(\<open>unbreabable\<close>" --- rare INCOMPATIBILITY.
    1.69  
    1.70  * Proof method "blast" is more robust wrt. corner cases of Pure
    1.71  statements without object-logic judgment.
    1.72  
    1.73 -* Pure provides basic versions of proof methods "simp" and "simp_all"
    1.74 -that only know about meta-equality (==). Potential INCOMPATIBILITY in
    1.75 -theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order
    1.76 -is relevant to avoid confusion of Pure.simp vs. HOL.simp.
    1.77 -
    1.78  * Commands 'prf' and 'full_prf' are somewhat more informative (again):
    1.79 -proof terms are reconstructed and cleaned from administrative thm
    1.80 -nodes.
    1.81 -
    1.82 -* The command 'unfolding' and proof method "unfold" include a second
    1.83 -stage where given equations are passed through the attribute "abs_def"
    1.84 -before rewriting. This ensures that definitions are fully expanded,
    1.85 -regardless of the actual parameters that are provided. Rare
    1.86 -INCOMPATIBILITY in some corner cases: use proof method (simp only:)
    1.87 -instead, or declare [[unfold_abs_def = false]] in the proof context.
    1.88 +proof terms are reconstructed and cleaned from administrative thm nodes.
    1.89 +
    1.90 +* Code generator: config option "code_timing" triggers measurements of
    1.91 +different phases of code generation. See src/HOL/ex/Code_Timing.thy for
    1.92 +examples.
    1.93 +
    1.94 +* Code generator: implicits in Scala (stemming from type class
    1.95 +instances) are generated into companion object of corresponding type
    1.96 +class, to resolve some situations where ambiguities may occur.
    1.97 +
    1.98 +* Splitter in simp, auto and friends:
    1.99 +  - The syntax "split add" has been discontinued, use plain "split",
   1.100 +    INCOMPATIBILITY.
   1.101 +  - For situations with many conditional or case expressions, there is
   1.102 +    an alternative splitting strategy that can be much faster. It is
   1.103 +    selected by writing "split!" instead of "split". It applies safe
   1.104 +    introduction and elimination rules after each split rule. As a
   1.105 +    result the subgoal may be split into several subgoals.
   1.106  
   1.107  
   1.108  *** Prover IDE -- Isabelle/Scala/jEdit ***
   1.109  
   1.110 +* Highlighting of entity def/ref positions wrt. cursor.
   1.111 +
   1.112 +* Action "isabelle.select-entity" (shortcut CS+ENTER) selects all
   1.113 +occurences of the formal entity at the caret position. This facilitates
   1.114 +systematic renaming.
   1.115 +
   1.116 +* PIDE document markup works across multiple Isar commands, e.g. the
   1.117 +results established at the end of a proof are properly identified in the
   1.118 +theorem statement.
   1.119 +
   1.120 +* Cartouche abbreviations work both for " and ` to accomodate typical
   1.121 +situations where old ASCII notation may be updated.
   1.122 +
   1.123  * Dockable window "Symbols" also provides access to 'abbrevs' from the
   1.124  outer syntax of the current theory buffer. This provides clickable
   1.125  syntax templates, including entries with empty abbrevs name (which are
   1.126  inaccessible via keyboard completion).
   1.127  
   1.128 -* Cartouche abbreviations work both for " and ` to accomodate typical
   1.129 -situations where old ASCII notation may be updated.
   1.130 -
   1.131 -* Isabelle/ML and Standard ML files are presented in Sidekick with the
   1.132 -tree structure of section headings: this special comment format is
   1.133 -described in "implementation" chapter 0, e.g. (*** section ***).
   1.134 -
   1.135  * IDE support for the Isabelle/Pure bootstrap process, with the
   1.136  following independent stages:
   1.137  
   1.138 @@ -116,11 +97,9 @@
   1.139  actual Isabelle/Pure that runs the IDE itself. The sequential
   1.140  dependencies of the above files are only observed for batch build.
   1.141  
   1.142 -* Highlighting of entity def/ref positions wrt. cursor.
   1.143 -
   1.144 -* Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed'
   1.145 -are treated as delimiters for fold structure; 'begin' and 'end'
   1.146 -structure of theory specifications is treated as well.
   1.147 +* Isabelle/ML and Standard ML files are presented in Sidekick with the
   1.148 +tree structure of section headings: this special comment format is
   1.149 +described in "implementation" chapter 0, e.g. (*** section ***).
   1.150  
   1.151  * Sidekick parser "isabelle-context" shows nesting of context blocks
   1.152  according to 'begin' and 'end' structure.
   1.153 @@ -138,9 +117,9 @@
   1.154  quickly; see also option "jedit_script_indent" and
   1.155  "jedit_script_indent_limit".
   1.156  
   1.157 -* Action "isabelle.select-entity" (shortcut CS+ENTER) selects all
   1.158 -occurences of the formal entity at the caret position. This facilitates
   1.159 -systematic renaming.
   1.160 +* Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed'
   1.161 +are treated as delimiters for fold structure; 'begin' and 'end'
   1.162 +structure of theory specifications is treated as well.
   1.163  
   1.164  * Action "isabelle.keymap-merge" asks the user to resolve pending
   1.165  Isabelle keymap changes that are in conflict with the current jEdit
   1.166 @@ -149,10 +128,6 @@
   1.167  increases chances that users see new keyboard shortcuts when re-using
   1.168  old keymaps.
   1.169  
   1.170 -* Document markup works across multiple Isar commands, e.g. the results
   1.171 -established at the end of a proof are properly identified in the theorem
   1.172 -statement.
   1.173 -
   1.174  * Command 'proof' provides information about proof outline with cases,
   1.175  e.g. for proof methods "cases", "induct", "goal_cases".
   1.176  
   1.177 @@ -179,19 +154,25 @@
   1.178  have to be changed.
   1.179  
   1.180  
   1.181 +*** Document preparation ***
   1.182 +
   1.183 +* New symbol \<circle>, e.g. for temporal operator.
   1.184 +
   1.185 +* Mixfix annotations support delimiters like \<^control>\<open>cartouche\<close> --
   1.186 +this allows special forms of document output.
   1.187 +
   1.188 +* Raw LaTeX output now works via \<^latex>\<open>...\<close> instead of raw control
   1.189 +symbol \<^raw:...>. INCOMPATIBILITY, notably for LaTeXsugar.thy and its
   1.190 +derivatives.
   1.191 +
   1.192 +* \<^raw:...> symbols are no longer supported.
   1.193 +
   1.194 +* Old 'header' command is no longer supported (legacy since
   1.195 +Isabelle2015).
   1.196 +
   1.197 +
   1.198  *** Isar ***
   1.199  
   1.200 -* The defining position of a literal fact \<open>prop\<close> is maintained more
   1.201 -carefully, and made accessible as hyperlink in the Prover IDE.
   1.202 -
   1.203 -* Commands 'finally' and 'ultimately' used to expose the result as
   1.204 -literal fact: this accidental behaviour has been discontinued. Rare
   1.205 -INCOMPATIBILITY, use more explicit means to refer to facts in Isar.
   1.206 -
   1.207 -* Command 'axiomatization' has become more restrictive to correspond
   1.208 -better to internal axioms as singleton facts with mandatory name. Minor
   1.209 -INCOMPATIBILITY.
   1.210 -
   1.211  * Many specification elements support structured statements with 'if' /
   1.212  'for' eigen-context, e.g. 'axiomatization', 'abbreviation',
   1.213  'definition', 'inductive', 'function'.
   1.214 @@ -213,8 +194,16 @@
   1.215  * Command '\<proof>' is an alias for 'sorry', with different
   1.216  typesetting. E.g. to produce proof holes in examples and documentation.
   1.217  
   1.218 -* The old proof method "default" has been removed (legacy since
   1.219 -Isabelle2016). INCOMPATIBILITY, use "standard" instead.
   1.220 +* The defining position of a literal fact \<open>prop\<close> is maintained more
   1.221 +carefully, and made accessible as hyperlink in the Prover IDE.
   1.222 +
   1.223 +* Commands 'finally' and 'ultimately' used to expose the result as
   1.224 +literal fact: this accidental behaviour has been discontinued. Rare
   1.225 +INCOMPATIBILITY, use more explicit means to refer to facts in Isar.
   1.226 +
   1.227 +* Command 'axiomatization' has become more restrictive to correspond
   1.228 +better to internal axioms as singleton facts with mandatory name. Minor
   1.229 +INCOMPATIBILITY.
   1.230  
   1.231  * Proof methods may refer to the main facts via the dynamic fact
   1.232  "method_facts". This is particularly useful for Eisbach method
   1.233 @@ -226,172 +215,54 @@
   1.234    (use facts in simp)
   1.235    (use facts in \<open>simp add: ...\<close>)
   1.236  
   1.237 +* The old proof method "default" has been removed (legacy since
   1.238 +Isabelle2016). INCOMPATIBILITY, use "standard" instead.
   1.239 +
   1.240  
   1.241  *** Pure ***
   1.242  
   1.243 -* Code generator: config option "code_timing" triggers measurements of
   1.244 -different phases of code generation. See src/HOL/ex/Code_Timing.thy for
   1.245 -examples.
   1.246 -
   1.247 -* Code generator: implicits in Scala (stemming from type class instances)
   1.248 -are generated into companion object of corresponding type class, to resolve
   1.249 -some situations where ambiguities may occur.
   1.250 +* Pure provides basic versions of proof methods "simp" and "simp_all"
   1.251 +that only know about meta-equality (==). Potential INCOMPATIBILITY in
   1.252 +theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order
   1.253 +is relevant to avoid confusion of Pure.simp vs. HOL.simp.
   1.254 +
   1.255 +* The command 'unfolding' and proof method "unfold" include a second
   1.256 +stage where given equations are passed through the attribute "abs_def"
   1.257 +before rewriting. This ensures that definitions are fully expanded,
   1.258 +regardless of the actual parameters that are provided. Rare
   1.259 +INCOMPATIBILITY in some corner cases: use proof method (simp only:)
   1.260 +instead, or declare [[unfold_abs_def = false]] in the proof context.
   1.261 +
   1.262 +* Type-inference improves sorts of newly introduced type variables for
   1.263 +the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL).
   1.264 +Thus terms like "f x" or "\<And>x. P x" without any further syntactic context
   1.265 +produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare
   1.266 +INCOMPATIBILITY, need to provide explicit type constraints for Pure
   1.267 +types where this is really intended.
   1.268  
   1.269  
   1.270  *** HOL ***
   1.271  
   1.272 -* New proof method "argo" using the built-in Argo solver based on SMT technology.
   1.273 -The method can be used to prove goals of quantifier-free propositional logic,
   1.274 -goals based on a combination of quantifier-free propositional logic with equality,
   1.275 -and goals based on a combination of quantifier-free propositional logic with
   1.276 -linear real arithmetic including min/max/abs. See HOL/ex/Argo_Examples.thy for
   1.277 -examples.
   1.278 -
   1.279 -* Type class "div" with operation "mod" renamed to type class "modulo" with
   1.280 -operation "modulo", analogously to type class "divide".  This eliminates the
   1.281 -need to qualify any of those names in the presence of infix "mod" syntax.
   1.282 -INCOMPATIBILITY.
   1.283 -
   1.284 -* The unique existence quantifier no longer provides 'binder' syntax,
   1.285 -but uses syntax translations (as for bounded unique existence). Thus
   1.286 -iterated quantification \<exists>!x y. P x y with its slightly confusing
   1.287 -sequential meaning \<exists>!x. \<exists>!y. P x y is no longer possible. Instead,
   1.288 -pattern abstraction admits simultaneous unique existence \<exists>!(x, y). P x y
   1.289 -(analogous to existing notation \<exists>!(x, y)\<in>A. P x y). Potential
   1.290 -INCOMPATIBILITY in rare situations.
   1.291 -
   1.292 -* Renamed session HOL-Multivariate_Analysis to HOL-Analysis.
   1.293 -
   1.294 -* Moved measure theory from HOL-Probability to HOL-Analysis. When importing
   1.295 -HOL-Analysis some theorems need additional name spaces prefixes due to name
   1.296 -clashes.
   1.297 -INCOMPATIBILITY.
   1.298 -
   1.299 -* In HOL-Probability the type of emeasure and nn_integral was changed
   1.300 -from ereal to ennreal:
   1.301 -  emeasure :: 'a measure => 'a set => ennreal
   1.302 -  nn_integral :: 'a measure => ('a => ennreal) => ennreal
   1.303 -INCOMPATIBILITY.
   1.304 -
   1.305 -* HOL-Analysis: more complex analysis including Cauchy's inequality, Liouville theorem,
   1.306 -open mapping theorem, maximum modulus principle, Residue theorem, Schwarz Lemma.
   1.307 -
   1.308 -* HOL-Analysis: Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman
   1.309 -Minkowski theorem.
   1.310 -
   1.311 -* HOL-Analysis: Numerous results ported from the HOL Light libraries: homeomorphisms,
   1.312 -continuous function extensions and other advanced topics in topology
   1.313 -
   1.314 -* Number_Theory: algebraic foundation for primes: Generalisation of
   1.315 -predicate "prime" and introduction of predicates "prime_elem",
   1.316 -"irreducible", a "prime_factorization" function, and the "factorial_ring"
   1.317 -typeclass with instance proofs for nat, int, poly. Some theorems now have
   1.318 -different names, most notably "prime_def" is now "prime_nat_iff".
   1.319 -INCOMPATIBILITY.
   1.320 -
   1.321 -* Probability: Code generation and QuickCheck for Probability Mass
   1.322 -Functions.
   1.323 -
   1.324 -* Theory Set_Interval.thy: substantial new theorems on indexed sums
   1.325 -and products.
   1.326 -
   1.327 -* Theory List.thy:
   1.328 -  listsum ~> sum_list
   1.329 -  listprod ~> prod_list
   1.330 -
   1.331 -* Theory Library/LaTeXsugar.thy: New style "dummy_pats" for displaying
   1.332 -equations in functional programming style: variables present on the
   1.333 -left-hand but not on the righ-hand side are replaced by underscores.
   1.334 -
   1.335 -* "surj" is a mere input abbreviation, to avoid hiding an equation in
   1.336 -term output.  Minor INCOMPATIBILITY.
   1.337 -
   1.338 -* Theory Library/Combinator_PER.thy: combinator to build partial
   1.339 -equivalence relations from a predicate and an equivalence relation.
   1.340 -
   1.341 -* Theory Library/Perm.thy: basic facts about almost everywhere fix
   1.342 -bijections.
   1.343 -
   1.344 -* Theory Library/Normalized_Fraction.thy: allows viewing an element
   1.345 -of a field of fractions as a normalized fraction (i.e. a pair of
   1.346 -numerator and denominator such that the two are coprime and the
   1.347 -denominator is normalized w.r.t. unit factors)
   1.348 -
   1.349 -* Locale bijection establishes convenient default simp rules
   1.350 -like "inv f (f a) = a" for total bijections.
   1.351 -
   1.352 -* Former locale lifting_syntax is now a bundle, which is easier to
   1.353 -include in a local context or theorem statement, e.g. "context includes
   1.354 -lifting_syntax begin ... end". Minor INCOMPATIBILITY.
   1.355 -
   1.356 -* Code generation for scala: ambiguous implicts in class diagrams
   1.357 -are spelt out explicitly.
   1.358 -
   1.359 -* Abstract locales semigroup, abel_semigroup, semilattice,
   1.360 -semilattice_neutr, ordering, ordering_top, semilattice_order,
   1.361 -semilattice_neutr_order, comm_monoid_set, semilattice_set,
   1.362 -semilattice_neutr_set, semilattice_order_set, semilattice_order_neutr_set
   1.363 -monoid_list, comm_monoid_list, comm_monoid_list_set, comm_monoid_mset,
   1.364 -comm_monoid_fun use boldified syntax uniformly that does not clash
   1.365 -with corresponding global syntax.  INCOMPATIBILITY.
   1.366 -
   1.367 -* Conventional syntax "%(). t" for unit abstractions.  Slight syntactic
   1.368 -INCOMPATIBILITY.
   1.369 -
   1.370 -* Command 'code_reflect' accepts empty constructor lists for datatypes,
   1.371 -which renders those abstract effectively.
   1.372 -
   1.373 -* Command 'export_code' checks given constants for abstraction violations:
   1.374 -a small guarantee that given constants specify a safe interface for the
   1.375 -generated code.
   1.376 -
   1.377 -* Probability/Random_Permutations.thy contains some theory about
   1.378 -choosing a permutation of a set uniformly at random and folding over a
   1.379 -list in random order.
   1.380 -
   1.381 -* Probability/SPMF formalises discrete subprobability distributions.
   1.382 -
   1.383 -* Library/FinFun.thy: bundles "finfun_syntax" and "no_finfun_syntax"
   1.384 -allow to control optional syntax in local contexts; this supersedes
   1.385 -former Library/FinFun_Syntax.thy. INCOMPATIBILITY, e.g. use "unbundle
   1.386 -finfun_syntax" to imitate import of "~~/src/HOL/Library/FinFun_Syntax".
   1.387 -
   1.388 -* Library/Set_Permutations.thy (executably) defines the set of
   1.389 -permutations of a set, i.e. the set of all lists that contain every
   1.390 -element of the carrier set exactly once.
   1.391 -
   1.392 -* Static evaluators (Code_Evaluation.static_* in Isabelle/ML) rely on
   1.393 -explicitly provided auxiliary definitions for required type class
   1.394 -dictionaries rather than half-working magic.  INCOMPATIBILITY, see
   1.395 -the tutorial on code generation for details.
   1.396 -
   1.397 -* New abbreviations for negated existence (but not bounded existence):
   1.398 -
   1.399 -  \<nexists>x. P x \<equiv> \<not> (\<exists>x. P x)
   1.400 -  \<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x)
   1.401 -
   1.402 -* The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@"
   1.403 -has been removed for output. It is retained for input only, until it is
   1.404 -eliminated altogether.
   1.405 -
   1.406 -* metis: The problem encoding has changed very slightly. This might
   1.407 +* New proof method "argo" using the built-in Argo solver based on SMT
   1.408 +technology. The method can be used to prove goals of quantifier-free
   1.409 +propositional logic, goals based on a combination of quantifier-free
   1.410 +propositional logic with equality, and goals based on a combination of
   1.411 +quantifier-free propositional logic with linear real arithmetic
   1.412 +including min/max/abs. See HOL/ex/Argo_Examples.thy for examples.
   1.413 +
   1.414 +* Metis: The problem encoding has changed very slightly. This might
   1.415  break existing proofs. INCOMPATIBILITY.
   1.416  
   1.417  * Sledgehammer:
   1.418    - The MaSh relevance filter is now faster than before.
   1.419    - Produce syntactically correct Vampire 4.0 problem files.
   1.420  
   1.421 -* The 'coinductive' command produces a proper coinduction rule for
   1.422 -mutual coinductive predicates. This new rule replaces the old rule,
   1.423 -which exposed details of the internal fixpoint construction and was
   1.424 -hard to use. INCOMPATIBILITY.
   1.425 -
   1.426  * (Co)datatype package:
   1.427    - New commands for defining corecursive functions and reasoning about
   1.428      them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive',
   1.429      'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof
   1.430      method. See 'isabelle doc corec'.
   1.431 -  - The predicator :: ('a => bool) => 'a F => bool is now a first-class
   1.432 +  - The predicator :: ('a \<Rightarrow> bool) \<Rightarrow> 'a F \<Rightarrow> bool is now a first-class
   1.433      citizen in bounded natural functors.
   1.434    - 'primrec' now allows nested calls through the predicator in addition
   1.435      to the map function.
   1.436 @@ -411,6 +282,100 @@
   1.437      equivalent) form.
   1.438      INCOMPATIBILITY.
   1.439  
   1.440 +* The 'coinductive' command produces a proper coinduction rule for
   1.441 +mutual coinductive predicates. This new rule replaces the old rule,
   1.442 +which exposed details of the internal fixpoint construction and was
   1.443 +hard to use. INCOMPATIBILITY.
   1.444 +
   1.445 +* New abbreviations for negated existence (but not bounded existence):
   1.446 +
   1.447 +  \<nexists>x. P x \<equiv> \<not> (\<exists>x. P x)
   1.448 +  \<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x)
   1.449 +
   1.450 +* The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@"
   1.451 +has been removed for output. It is retained for input only, until it is
   1.452 +eliminated altogether.
   1.453 +
   1.454 +* The unique existence quantifier no longer provides 'binder' syntax,
   1.455 +but uses syntax translations (as for bounded unique existence). Thus
   1.456 +iterated quantification \<exists>!x y. P x y with its slightly confusing
   1.457 +sequential meaning \<exists>!x. \<exists>!y. P x y is no longer possible. Instead,
   1.458 +pattern abstraction admits simultaneous unique existence \<exists>!(x, y). P x y
   1.459 +(analogous to existing notation \<exists>!(x, y)\<in>A. P x y). Potential
   1.460 +INCOMPATIBILITY in rare situations.
   1.461 +
   1.462 +* Conventional syntax "%(). t" for unit abstractions. Slight syntactic
   1.463 +INCOMPATIBILITY.
   1.464 +
   1.465 +* Characters (type char) are modelled as finite algebraic type
   1.466 +corresponding to {0..255}.
   1.467 +
   1.468 +  - Logical representation:
   1.469 +    * 0 is instantiated to the ASCII zero character.
   1.470 +    * All other characters are represented as "Char n"
   1.471 +      with n being a raw numeral expression less than 256.
   1.472 +    * Expressions of the form "Char n" with n greater than 255
   1.473 +      are non-canonical.
   1.474 +  - Printing and parsing:
   1.475 +    * Printable characters are printed and parsed as "CHR ''\<dots>''"
   1.476 +      (as before).
   1.477 +    * The ASCII zero character is printed and parsed as "0".
   1.478 +    * All other canonical characters are printed as "CHR 0xXX"
   1.479 +      with XX being the hexadecimal character code.  "CHR n"
   1.480 +      is parsable for every numeral expression n.
   1.481 +    * Non-canonical characters have no special syntax and are
   1.482 +      printed as their logical representation.
   1.483 +  - Explicit conversions from and to the natural numbers are
   1.484 +    provided as char_of_nat, nat_of_char (as before).
   1.485 +  - The auxiliary nibble type has been discontinued.
   1.486 +
   1.487 +INCOMPATIBILITY.
   1.488 +
   1.489 +* Type class "div" with operation "mod" renamed to type class "modulo"
   1.490 +with operation "modulo", analogously to type class "divide". This
   1.491 +eliminates the need to qualify any of those names in the presence of
   1.492 +infix "mod" syntax. INCOMPATIBILITY.
   1.493 +
   1.494 +* Constant "surj" is a mere input abbreviation, to avoid hiding an
   1.495 +equation in term output. Minor INCOMPATIBILITY.
   1.496 +
   1.497 +* Command 'code_reflect' accepts empty constructor lists for datatypes,
   1.498 +which renders those abstract effectively.
   1.499 +
   1.500 +* Command 'export_code' checks given constants for abstraction
   1.501 +violations: a small guarantee that given constants specify a safe
   1.502 +interface for the generated code.
   1.503 +
   1.504 +* Code generation for Scala: ambiguous implicts in class diagrams are
   1.505 +spelt out explicitly.
   1.506 +
   1.507 +* Static evaluators (Code_Evaluation.static_* in Isabelle/ML) rely on
   1.508 +explicitly provided auxiliary definitions for required type class
   1.509 +dictionaries rather than half-working magic.  INCOMPATIBILITY, see
   1.510 +the tutorial on code generation for details.
   1.511 +
   1.512 +* Theory Set_Interval.thy: substantial new theorems on indexed sums
   1.513 +and products.
   1.514 +
   1.515 +* Theory List.thy: ranaming of listsum ~> sum_list, listprod ~>
   1.516 +prod_list, INCOMPATIBILITY.
   1.517 +
   1.518 +* Locale bijection establishes convenient default simp rules such as
   1.519 +"inv f (f a) = a" for total bijections.
   1.520 +
   1.521 +* Abstract locales semigroup, abel_semigroup, semilattice,
   1.522 +semilattice_neutr, ordering, ordering_top, semilattice_order,
   1.523 +semilattice_neutr_order, comm_monoid_set, semilattice_set,
   1.524 +semilattice_neutr_set, semilattice_order_set,
   1.525 +semilattice_order_neutr_set monoid_list, comm_monoid_list,
   1.526 +comm_monoid_list_set, comm_monoid_mset, comm_monoid_fun use boldified
   1.527 +syntax uniformly that does not clash with corresponding global syntax.
   1.528 +INCOMPATIBILITY.
   1.529 +
   1.530 +* Former locale lifting_syntax is now a bundle, which is easier to
   1.531 +include in a local context or theorem statement, e.g. "context includes
   1.532 +lifting_syntax begin ... end". Minor INCOMPATIBILITY.
   1.533 +
   1.534  * Some old / obsolete theorems have been renamed / removed, potential
   1.535  INCOMPATIBILITY.
   1.536  
   1.537 @@ -444,31 +409,20 @@
   1.538  * Renamed split_if -> if_split and split_if_asm -> if_split_asm to
   1.539  resemble the f.split naming convention, INCOMPATIBILITY.
   1.540  
   1.541 -* Characters (type char) are modelled as finite algebraic type
   1.542 -corresponding to {0..255}.
   1.543 -
   1.544 -  - Logical representation:
   1.545 -    * 0 is instantiated to the ASCII zero character.
   1.546 -    * All other characters are represented as "Char n"
   1.547 -      with n being a raw numeral expression less than 256.
   1.548 -    * Expressions of the form "Char n" with n greater than 255
   1.549 -      are non-canonical.
   1.550 -  - Printing and parsing:
   1.551 -    * Printable characters are printed and parsed as "CHR ''\<dots>''"
   1.552 -      (as before).
   1.553 -    * The ASCII zero character is printed and parsed as "0".
   1.554 -    * All other canonical characters are printed as "CHR 0xXX"
   1.555 -      with XX being the hexadecimal character code.  "CHR n"
   1.556 -      is parsable for every numeral expression n.
   1.557 -    * Non-canonical characters have no special syntax and are
   1.558 -      printed as their logical representation.
   1.559 -  - Explicit conversions from and to the natural numbers are
   1.560 -    provided as char_of_nat, nat_of_char (as before).
   1.561 -  - The auxiliary nibble type has been discontinued.
   1.562 -
   1.563 -INCOMPATIBILITY.
   1.564 -
   1.565 -* Multiset membership is now expressed using set_mset rather than count.
   1.566 +* Added class topological_monoid.
   1.567 +
   1.568 +* HOL-Library: theory FinFun bundles "finfun_syntax" and
   1.569 +"no_finfun_syntax" allow to control optional syntax in local contexts;
   1.570 +this supersedes former theory FinFun_Syntax. INCOMPATIBILITY, e.g. use
   1.571 +"unbundle finfun_syntax" to imitate import of
   1.572 +"~~/src/HOL/Library/FinFun_Syntax".
   1.573 +
   1.574 +* HOL-Library: theory Set_Permutations (executably) defines the set of
   1.575 +permutations of a set, i.e. the set of all lists that contain every
   1.576 +element of the carrier set exactly once.
   1.577 +
   1.578 +* HOL-Library: multiset membership is now expressed using set_mset
   1.579 +rather than count.
   1.580  
   1.581    - Expressions "count M a > 0" and similar simplify to membership
   1.582      by default.
   1.583 @@ -484,8 +438,68 @@
   1.584  
   1.585  INCOMPATIBILITY.
   1.586  
   1.587 -* The names of multiset theorems have been normalised to distinguish which
   1.588 -  ordering the theorems are about
   1.589 +* HOL-Library: theory LaTeXsugar uses new-style "dummy_pats" for
   1.590 +displaying equations in functional programming style --- variables
   1.591 +present on the left-hand but not on the righ-hand side are replaced by
   1.592 +underscores.
   1.593 +
   1.594 +* HOL-Library: theory Combinator_PER provides combinator to build
   1.595 +partial equivalence relations from a predicate and an equivalence
   1.596 +relation.
   1.597 +
   1.598 +* HOL-Library: theory Perm provides basic facts about almost everywhere
   1.599 +fix bijections.
   1.600 +
   1.601 +* HOL-Library: theory Normalized_Fraction allows viewing an element of a
   1.602 +field of fractions as a normalized fraction (i.e. a pair of numerator
   1.603 +and denominator such that the two are coprime and the denominator is
   1.604 +normalized wrt. unit factors).
   1.605 +
   1.606 +* Session HOL-NSA has been renamed to HOL-Nonstandard_Analysis.
   1.607 +
   1.608 +* Session HOL-Multivariate_Analysis has been renamed to HOL-Analysis.
   1.609 +
   1.610 +* HOL-Analysis: measure theory has been moved here from HOL-Probability.
   1.611 +When importing HOL-Analysis some theorems need additional name spaces
   1.612 +prefixes due to name clashes. INCOMPATIBILITY.
   1.613 +
   1.614 +* HOL-Analysis: more complex analysis including Cauchy's inequality,
   1.615 +Liouville theorem, open mapping theorem, maximum modulus principle,
   1.616 +Residue theorem, Schwarz Lemma.
   1.617 +
   1.618 +* HOL-Analysis: Theory of polyhedra: faces, extreme points, polytopes,
   1.619 +and the Krein–Milman Minkowski theorem.
   1.620 +
   1.621 +* HOL-Analysis: Numerous results ported from the HOL Light libraries:
   1.622 +homeomorphisms, continuous function extensions and other advanced topics
   1.623 +in topology
   1.624 +
   1.625 +* HOL-Probability: the type of emeasure and nn_integral was changed from
   1.626 +ereal to ennreal, INCOMPATIBILITY.
   1.627 +
   1.628 +  emeasure :: 'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal
   1.629 +  nn_integral :: 'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ennreal
   1.630 +
   1.631 +* HOL-Probability: Code generation and QuickCheck for Probability Mass
   1.632 +Functions.
   1.633 +
   1.634 +* HOL-Probability: theory Random_Permutations contains some theory about
   1.635 +choosing a permutation of a set uniformly at random and folding over a
   1.636 +list in random order.
   1.637 +
   1.638 +* HOL-Probability: theory SPMF formalises discrete subprobability
   1.639 +distributions.
   1.640 +
   1.641 +* HOL-Number_Theory: algebraic foundation for primes: Generalisation of
   1.642 +predicate "prime" and introduction of predicates "prime_elem",
   1.643 +"irreducible", a "prime_factorization" function, and the
   1.644 +"factorial_ring" typeclass with instance proofs for nat, int, poly. Some
   1.645 +theorems now have different names, most notably "prime_def" is now
   1.646 +"prime_nat_iff". INCOMPATIBILITY.
   1.647 +
   1.648 +* HOL-Library: the names of multiset theorems have been normalised to
   1.649 +distinguish which ordering the theorems are about
   1.650 +
   1.651      mset_less_eqI ~> mset_subset_eqI
   1.652      mset_less_insertD ~> mset_subset_insertD
   1.653      mset_less_eq_count ~> mset_subset_eq_count
   1.654 @@ -512,23 +526,25 @@
   1.655      mset_remdups_le ~> mset_remdups_subset_eq
   1.656      ms_lesseq_impl ~> subset_eq_mset_impl
   1.657  
   1.658 -  Some functions have been renamed:
   1.659 +Some functions have been renamed:
   1.660      ms_lesseq_impl -> subset_eq_mset_impl
   1.661  
   1.662 -* Multisets are now ordered with the multiset ordering
   1.663 +* HOL-Library: multisets are now ordered with the multiset ordering
   1.664      #\<subseteq># ~> \<le>
   1.665      #\<subset># ~> <
   1.666      le_multiset ~> less_eq_multiset
   1.667      less_multiset ~> le_multiset
   1.668  INCOMPATIBILITY.
   1.669  
   1.670 -* The prefix multiset_order has been discontinued: the theorems can be directly
   1.671 -accessed. As a consequence, the lemmas "order_multiset" and "linorder_multiset"
   1.672 -have been discontinued, and the interpretations "multiset_linorder" and
   1.673 -"multiset_wellorder" have been replaced by instantiations.
   1.674 -INCOMPATIBILITY.
   1.675 -
   1.676 -* Some theorems about the multiset ordering have been renamed:
   1.677 +* HOL-Library: the prefix multiset_order has been discontinued: the
   1.678 +theorems can be directly accessed. As a consequence, the lemmas
   1.679 +"order_multiset" and "linorder_multiset" have been discontinued, and the
   1.680 +interpretations "multiset_linorder" and "multiset_wellorder" have been
   1.681 +replaced by instantiations. INCOMPATIBILITY.
   1.682 +
   1.683 +* HOL-Library: some theorems about the multiset ordering have been
   1.684 +renamed:
   1.685 +
   1.686      le_multiset_def ~> less_eq_multiset_def
   1.687      less_multiset_def ~> le_multiset_def
   1.688      less_eq_imp_le_multiset ~> subset_eq_imp_le_multiset
   1.689 @@ -554,32 +570,36 @@
   1.690      less_multiset_plus_plus_right_iff ~> le_multiset_plus_plus_right_iff
   1.691  INCOMPATIBILITY.
   1.692  
   1.693 -* The lemma mset_map has now the attribute [simp].
   1.694 -INCOMPATIBILITY.
   1.695 -
   1.696 -* Some theorems about multisets have been removed:
   1.697 +* HOL-Library: the lemma mset_map has now the attribute [simp].
   1.698 +INCOMPATIBILITY.
   1.699 +
   1.700 +* HOL-Library: some theorems about multisets have been removed.
   1.701 +INCOMPATIBILITY, use the following replacements:
   1.702 +
   1.703      le_multiset_plus_plus_left_iff ~> add_less_cancel_right
   1.704      le_multiset_plus_plus_right_iff ~> add_less_cancel_left
   1.705      add_eq_self_empty_iff ~> add_cancel_left_right
   1.706      mset_subset_add_bothsides ~> subset_mset.add_less_cancel_right
   1.707 -INCOMPATIBILITY.
   1.708 -
   1.709 -* Some typeclass constraints about multisets have been reduced from ordered or
   1.710 -linordered to preorder. Multisets have the additional typeclasses order_bot,
   1.711 -no_top, ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add,
   1.712 -linordered_cancel_ab_semigroup_add, and ordered_ab_semigroup_monoid_add_imp_le.
   1.713 -INCOMPATIBILITY.
   1.714 -
   1.715 -* There are some new simplification rules about multisets, the multiset
   1.716 -ordering, and the subset ordering on multisets.
   1.717 -INCOMPATIBILITY.
   1.718 -
   1.719 -* The subset ordering on multisets has now the interpretations
   1.720 -ordered_ab_semigroup_monoid_add_imp_le and bounded_lattice_bot.
   1.721 -INCOMPATIBILITY.
   1.722 -
   1.723 -* Multiset: single has been removed in favor of add_mset that roughly
   1.724 -corresponds to Set.insert. Some theorems have removed or changed:
   1.725 +
   1.726 +* HOL-Library: some typeclass constraints about multisets have been
   1.727 +reduced from ordered or linordered to preorder. Multisets have the
   1.728 +additional typeclasses order_bot, no_top,
   1.729 +ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add,
   1.730 +linordered_cancel_ab_semigroup_add, and
   1.731 +ordered_ab_semigroup_monoid_add_imp_le. INCOMPATIBILITY.
   1.732 +
   1.733 +* HOL-Library: there are some new simplification rules about multisets,
   1.734 +the multiset ordering, and the subset ordering on multisets.
   1.735 +INCOMPATIBILITY.
   1.736 +
   1.737 +* HOL-Library: the subset ordering on multisets has now the
   1.738 +interpretations ordered_ab_semigroup_monoid_add_imp_le and
   1.739 +bounded_lattice_bot. INCOMPATIBILITY.
   1.740 +
   1.741 +* HOL-Library/Multiset: single has been removed in favor of add_mset
   1.742 +that roughly corresponds to Set.insert. Some theorems have removed or
   1.743 +changed:
   1.744 +
   1.745    single_not_empty ~> add_mset_not_empty or empty_not_add_mset
   1.746    fold_mset_insert ~> fold_mset_add_mset
   1.747    image_mset_insert ~> image_mset_add_mset
   1.748 @@ -588,7 +608,9 @@
   1.749    diff_single_eq_union
   1.750  INCOMPATIBILITY.
   1.751  
   1.752 -* Multiset: some theorems have been changed to use add_mset instead of single:
   1.753 +* HOL-Library/Multiset: some theorems have been changed to use add_mset
   1.754 +instead of single:
   1.755 +
   1.756    mset_add
   1.757    multi_self_add_other_not_self
   1.758    diff_single_eq_union
   1.759 @@ -630,8 +652,8 @@
   1.760    multiset_induct2
   1.761  INCOMPATIBILITY.
   1.762  
   1.763 -* Multiset: the definitions of some constants have changed to use add_mset instead
   1.764 -of adding a single element:
   1.765 +* HOL-Library/Multiset. The definitions of some constants have changed
   1.766 +to use add_mset instead of adding a single element:
   1.767    image_mset
   1.768    mset
   1.769    replicate_mset
   1.770 @@ -641,8 +663,8 @@
   1.771    mset_insort
   1.772  INCOMPATIBILITY.
   1.773  
   1.774 -* Due to the above changes, the attributes of some multiset theorems have
   1.775 -been changed:
   1.776 +* HOL-Library/Multiset. Due to the above changes, the attributes of some
   1.777 +multiset theorems have been changed:
   1.778    insert_DiffM  [] ~> [simp]
   1.779    insert_DiffM2 [simp] ~> []
   1.780    diff_add_mset_swap [simp]
   1.781 @@ -664,26 +686,26 @@
   1.782    empty_inter [simp] ~> []
   1.783  INCOMPATIBILITY.
   1.784  
   1.785 -* The order of the variables in the second cases of multiset_induct,
   1.786 -multiset_induct2_size, multiset_induct2 has been changed (e.g. Add A a ~> Add a A).
   1.787 -INCOMPATIBILITY.
   1.788 -
   1.789 -* There is now a simplification procedure on multisets. It mimics the behavior
   1.790 -of the procedure on natural numbers.
   1.791 -INCOMPATIBILITY.
   1.792 -
   1.793 -* Renamed sums and products of multisets:
   1.794 +* HOL-Library/Multiset. The order of the variables in the second cases
   1.795 +of multiset_induct, multiset_induct2_size, multiset_induct2 has been
   1.796 +changed (e.g. Add A a ~> Add a A). INCOMPATIBILITY.
   1.797 +
   1.798 +* HOL-Library/Multiset. There is now a simplification procedure on
   1.799 +multisets. It mimics the behavior of the procedure on natural numbers.
   1.800 +INCOMPATIBILITY.
   1.801 +
   1.802 +* HOL-Library/Multiset. Renamed sums and products of multisets:
   1.803    msetsum ~> sum_mset
   1.804    msetprod ~> prod_mset
   1.805  
   1.806 -* The symbols for intersection and union of multisets have been changed:
   1.807 +* HOL-Library/Multiset. The notation for intersection and union of
   1.808 +multisets have been changed:
   1.809    #\<inter> ~> \<inter>#
   1.810    #\<union> ~> \<union>#
   1.811  INCOMPATIBILITY.
   1.812  
   1.813 -* The lemma one_step_implies_mult_aux on multisets has been removed, use
   1.814 -one_step_implies_mult instead.
   1.815 -INCOMPATIBILITY.
   1.816 +* HOL-Library/Multiset. The lemma one_step_implies_mult_aux on multisets
   1.817 +has been removed, use one_step_implies_mult instead. INCOMPATIBILITY.
   1.818  
   1.819  * The following theorems have been renamed:
   1.820    setsum_left_distrib ~> setsum_distrib_right
   1.821 @@ -699,36 +721,37 @@
   1.822  * Class semiring_Lcd merged into semiring_Gcd.  INCOMPATIBILITY.
   1.823  
   1.824  * The type class ordered_comm_monoid_add is now called
   1.825 -ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add is
   1.826 -introduced as the combination of ordered_ab_semigroup_add + comm_monoid_add.
   1.827 -INCOMPATIBILITY.
   1.828 -
   1.829 -* Introduced the type classes canonically_ordered_comm_monoid_add and dioid.
   1.830 +ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add
   1.831 +is introduced as the combination of ordered_ab_semigroup_add +
   1.832 +comm_monoid_add. INCOMPATIBILITY.
   1.833 +
   1.834 +* Introduced the type classes canonically_ordered_comm_monoid_add and
   1.835 +dioid.
   1.836  
   1.837  * Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When
   1.838 -instantiating linordered_semiring_strict and ordered_ab_group_add, an explicit
   1.839 -instantiation of ordered_ab_semigroup_monoid_add_imp_le might be
   1.840 -required.
   1.841 -INCOMPATIBILITY.
   1.842 -
   1.843 -* Added topological_monoid
   1.844 -
   1.845 -* Library/Complete_Partial_Order2.thy provides reasoning support for
   1.846 -proofs about monotonicity and continuity in chain-complete partial
   1.847 -orders and about admissibility conditions for fixpoint inductions.
   1.848 -
   1.849 -* Library/Polynomial.thy contains also derivation of polynomials
   1.850 -but not gcd/lcm on polynomials over fields.  This has been moved
   1.851 -to a separate theory Library/Polynomial_GCD_euclidean.thy, to
   1.852 -pave way for a possible future different type class instantiation
   1.853 -for polynomials over factorial rings.  INCOMPATIBILITY.
   1.854 -
   1.855 -* Library/Sublist.thy: added function "prefixes" and renamed
   1.856 +instantiating linordered_semiring_strict and ordered_ab_group_add, an
   1.857 +explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might
   1.858 +be required. INCOMPATIBILITY.
   1.859 +
   1.860 +* HOL-Library: theory Complete_Partial_Order2 provides reasoning support
   1.861 +for monotonicity and continuity in chain-complete partial orders and
   1.862 +about admissibility conditions for fixpoint inductions.
   1.863 +
   1.864 +* HOL-Library: theory Polynomial contains also derivation of polynomials
   1.865 +but not gcd/lcm on polynomials over fields. This has been moved to a
   1.866 +separate theory Library/Polynomial_GCD_euclidean.thy, to pave way for a
   1.867 +possible future different type class instantiation for polynomials over
   1.868 +factorial rings. INCOMPATIBILITY.
   1.869 +
   1.870 +* HOL-Library: theory Sublist.thy provides function "prefixes" with the
   1.871 +following renaming
   1.872 +
   1.873    prefixeq -> prefix
   1.874    prefix -> strict_prefix
   1.875    suffixeq -> suffix
   1.876    suffix -> strict_suffix
   1.877 -  Added theory of longest common prefixes.
   1.878 +
   1.879 +Added theory of longest common prefixes.
   1.880  
   1.881  * Dropped various legacy fact bindings, whose replacements are often
   1.882  of a more general type also:
   1.883 @@ -822,11 +845,9 @@
   1.884    dvd_Gcd, dvd_Gcd_nat, dvd_Gcd_int removed in favour of Gcd_greatest
   1.885  INCOMPATIBILITY.
   1.886  
   1.887 -* Session HOL-NSA has been renamed to HOL-Nonstandard_Analysis.
   1.888 -
   1.889  * Renamed HOL/Quotient_Examples/FSet.thy to
   1.890 -HOL/Quotient_Examples/Quotient_FSet.thy
   1.891 -INCOMPATIBILITY.
   1.892 +HOL/Quotient_Examples/Quotient_FSet.thy INCOMPATIBILITY.
   1.893 +
   1.894  
   1.895  *** ML ***
   1.896