misc tuning for release;
authorwenzelm
Tue Oct 25 11:55:38 2016 +0200 (2016-10-25)
changeset 64390ad2c5f37f659
parent 64389 6273d4c8325b
child 64391 553d8c4d7ef4
child 64394 141e1ed8d5a0
misc tuning for release;
NEWS
     1.1 --- a/NEWS	Mon Oct 24 22:42:07 2016 +0200
     1.2 +++ b/NEWS	Tue Oct 25 11:55:38 2016 +0200
     1.3 @@ -9,6 +9,15 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Splitter in proof methods "simp", "auto" and friends:
     1.8 +  - The syntax "split add" has been discontinued, use plain "split",
     1.9 +    INCOMPATIBILITY.
    1.10 +  - For situations with many conditional or case expressions, there is
    1.11 +    an alternative splitting strategy that can be much faster. It is
    1.12 +    selected by writing "split!" instead of "split". It applies safe
    1.13 +    introduction and elimination rules after each split rule. As a
    1.14 +    result the subgoal may be split into several subgoals.
    1.15 +
    1.16  * Command 'bundle' provides a local theory target to define a bundle
    1.17  from the body of specification commands (such as 'declare',
    1.18  'declaration', 'notation', 'lemmas', 'lemma'). For example:
    1.19 @@ -51,21 +60,38 @@
    1.20  instances) are generated into companion object of corresponding type
    1.21  class, to resolve some situations where ambiguities may occur.
    1.22  
    1.23 -* Splitter in simp, auto and friends:
    1.24 -  - The syntax "split add" has been discontinued, use plain "split",
    1.25 -    INCOMPATIBILITY.
    1.26 -  - For situations with many conditional or case expressions, there is
    1.27 -    an alternative splitting strategy that can be much faster. It is
    1.28 -    selected by writing "split!" instead of "split". It applies safe
    1.29 -    introduction and elimination rules after each split rule. As a
    1.30 -    result the subgoal may be split into several subgoals.
    1.31 -
    1.32 -* Solve direct: option 'solve_direct_strict_warnings' gives explicit
    1.33 -  warnings for lemma statements with trivial proofs.
    1.34 +* Solve direct: option "solve_direct_strict_warnings" gives explicit
    1.35 +warnings for lemma statements with trivial proofs.
    1.36  
    1.37  
    1.38  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.39  
    1.40 +* Syntactic indentation according to Isabelle outer syntax. Action
    1.41 +"indent-lines" (shortcut C+i) indents the current line according to
    1.42 +command keywords and some command substructure. Action
    1.43 +"isabelle.newline" (shortcut ENTER) indents the old and the new line
    1.44 +according to command keywords only; see also option
    1.45 +"jedit_indent_newline".
    1.46 +
    1.47 +* Semantic indentation for unstructured proof scripts ('apply' etc.) via
    1.48 +number of subgoals. This requires information of ongoing document
    1.49 +processing and may thus lag behind, when the user is editing too
    1.50 +quickly; see also option "jedit_script_indent" and
    1.51 +"jedit_script_indent_limit".
    1.52 +
    1.53 +* Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed'
    1.54 +are treated as delimiters for fold structure; 'begin' and 'end'
    1.55 +structure of theory specifications is treated as well.
    1.56 +
    1.57 +* Command 'proof' provides information about proof outline with cases,
    1.58 +e.g. for proof methods "cases", "induct", "goal_cases".
    1.59 +
    1.60 +* Completion templates for commands involving "begin ... end" blocks,
    1.61 +e.g. 'context', 'notepad'.
    1.62 +
    1.63 +* Sidekick parser "isabelle-context" shows nesting of context blocks
    1.64 +according to 'begin' and 'end' structure.
    1.65 +
    1.66  * Highlighting of entity def/ref positions wrt. cursor.
    1.67  
    1.68  * Action "isabelle.select-entity" (shortcut CS+ENTER) selects all
    1.69 @@ -104,39 +130,6 @@
    1.70  tree structure of section headings: this special comment format is
    1.71  described in "implementation" chapter 0, e.g. (*** section ***).
    1.72  
    1.73 -* Sidekick parser "isabelle-context" shows nesting of context blocks
    1.74 -according to 'begin' and 'end' structure.
    1.75 -
    1.76 -* Syntactic indentation according to Isabelle outer syntax. Action
    1.77 -"indent-lines" (shortcut C+i) indents the current line according to
    1.78 -command keywords and some command substructure. Action
    1.79 -"isabelle.newline" (shortcut ENTER) indents the old and the new line
    1.80 -according to command keywords only; see also option
    1.81 -"jedit_indent_newline".
    1.82 -
    1.83 -* Semantic indentation for unstructured proof scripts ('apply' etc.) via
    1.84 -number of subgoals. This requires information of ongoing document
    1.85 -processing and may thus lag behind, when the user is editing too
    1.86 -quickly; see also option "jedit_script_indent" and
    1.87 -"jedit_script_indent_limit".
    1.88 -
    1.89 -* Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed'
    1.90 -are treated as delimiters for fold structure; 'begin' and 'end'
    1.91 -structure of theory specifications is treated as well.
    1.92 -
    1.93 -* Action "isabelle.keymap-merge" asks the user to resolve pending
    1.94 -Isabelle keymap changes that are in conflict with the current jEdit
    1.95 -keymap; non-conflicting changes are always applied implicitly. This
    1.96 -action is automatically invoked on Isabelle/jEdit startup and thus
    1.97 -increases chances that users see new keyboard shortcuts when re-using
    1.98 -old keymaps.
    1.99 -
   1.100 -* Command 'proof' provides information about proof outline with cases,
   1.101 -e.g. for proof methods "cases", "induct", "goal_cases".
   1.102 -
   1.103 -* Completion templates for commands involving "begin ... end" blocks,
   1.104 -e.g. 'context', 'notepad'.
   1.105 -
   1.106  * Additional abbreviations for syntactic completion may be specified
   1.107  within the theory header as 'abbrevs'. The theory syntax for 'keywords'
   1.108  has been simplified accordingly: optional abbrevs need to go into the
   1.109 @@ -146,6 +139,13 @@
   1.110  $ISABELLE_HOME_USER/etc/abbrevs are no longer supported. Minor
   1.111  INCOMPATIBILITY, use 'abbrevs' within theory header instead.
   1.112  
   1.113 +* Action "isabelle.keymap-merge" asks the user to resolve pending
   1.114 +Isabelle keymap changes that are in conflict with the current jEdit
   1.115 +keymap; non-conflicting changes are always applied implicitly. This
   1.116 +action is automatically invoked on Isabelle/jEdit startup and thus
   1.117 +increases chances that users see new keyboard shortcuts when re-using
   1.118 +old keymaps.
   1.119 +
   1.120  * ML and document antiquotations for file-systems paths are more uniform
   1.121  and diverse:
   1.122  
   1.123 @@ -249,49 +249,6 @@
   1.124  
   1.125  *** HOL ***
   1.126  
   1.127 -* Ported remaining theories of Old_Number_Theory and removed Old_Number_Theory.
   1.128 -
   1.129 -* Sligthly more standardized theorem names:
   1.130 -    sgn_times ~> sgn_mult
   1.131 -    sgn_mult' ~> Real_Vector_Spaces.sgn_mult
   1.132 -    divide_zero_left ~> div_0
   1.133 -    zero_mod_left ~> mod_0
   1.134 -    divide_zero ~> div_by_0
   1.135 -    divide_1 ~> div_by_1
   1.136 -    nonzero_mult_divide_cancel_left ~> nonzero_mult_div_cancel_left
   1.137 -    div_mult_self1_is_id ~> nonzero_mult_div_cancel_left
   1.138 -    nonzero_mult_divide_cancel_right ~> nonzero_mult_div_cancel_right
   1.139 -    div_mult_self2_is_id ~> nonzero_mult_div_cancel_right
   1.140 -    is_unit_divide_mult_cancel_left ~> is_unit_div_mult_cancel_left
   1.141 -    is_unit_divide_mult_cancel_right ~> is_unit_div_mult_cancel_right
   1.142 -    mod_div_equality ~> div_mult_mod_eq
   1.143 -    mod_div_equality2 ~> mult_div_mod_eq
   1.144 -    mod_div_equality3 ~> mod_div_mult_eq
   1.145 -    mod_div_equality4 ~> mod_mult_div_eq
   1.146 -    minus_div_eq_mod ~> minus_div_mult_eq_mod
   1.147 -    minus_div_eq_mod2 ~> minus_mult_div_eq_mod
   1.148 -    minus_mod_eq_div ~> minus_mod_eq_div_mult
   1.149 -    minus_mod_eq_div2 ~> minus_mod_eq_mult_div
   1.150 -    div_mod_equality' ~> minus_mod_eq_div_mult [symmetric]
   1.151 -    mod_div_equality' ~> minus_div_mult_eq_mod [symmetric]
   1.152 -    zmod_zdiv_equality ~> mult_div_mod_eq [symmetric]
   1.153 -    zmod_zdiv_equality' ~> minus_div_mult_eq_mod [symmetric]
   1.154 -    Divides.mult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
   1.155 -    mult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
   1.156 -    zmult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
   1.157 -    div_1 ~> div_by_Suc_0
   1.158 -    mod_1 ~> mod_by_Suc_0
   1.159 -INCOMPATIBILITY.
   1.160 -
   1.161 -* Renamed constants "setsum" ~> "sum" and "setprod" ~> "prod".
   1.162 -  Corresponding renaming of theorems.
   1.163 -
   1.164 -* New type class "idom_abs_sgn" specifies algebraic properties
   1.165 -of sign and absolute value functions.  Type class "sgn_if" has
   1.166 -disappeared.  Slight INCOMPATIBILITY.
   1.167 -
   1.168 -* Dedicated syntax LENGTH('a) for length of types.
   1.169 -
   1.170  * New proof method "argo" using the built-in Argo solver based on SMT
   1.171  technology. The method can be used to prove goals of quantifier-free
   1.172  propositional logic, goals based on a combination of quantifier-free
   1.173 @@ -299,6 +256,9 @@
   1.174  quantifier-free propositional logic with linear real arithmetic
   1.175  including min/max/abs. See HOL/ex/Argo_Examples.thy for examples.
   1.176  
   1.177 +* The new "nunchaku" program integrates the Nunchaku model finder. The
   1.178 +tool is experimental. See ~~/src/HOL/Nunchaku/Nunchaku.thy for details.
   1.179 +
   1.180  * Metis: The problem encoding has changed very slightly. This might
   1.181  break existing proofs. INCOMPATIBILITY.
   1.182  
   1.183 @@ -356,6 +316,53 @@
   1.184  * Conventional syntax "%(). t" for unit abstractions. Slight syntactic
   1.185  INCOMPATIBILITY.
   1.186  
   1.187 +* Renamed constants and corresponding theorems:
   1.188 +
   1.189 +    setsum ~> sum
   1.190 +    setprod ~> prod
   1.191 +    listsum ~> sum_list
   1.192 +    listprod ~> prod_list
   1.193 +
   1.194 +INCOMPATIBILITY.
   1.195 +
   1.196 +* Sligthly more standardized theorem names:
   1.197 +    sgn_times ~> sgn_mult
   1.198 +    sgn_mult' ~> Real_Vector_Spaces.sgn_mult
   1.199 +    divide_zero_left ~> div_0
   1.200 +    zero_mod_left ~> mod_0
   1.201 +    divide_zero ~> div_by_0
   1.202 +    divide_1 ~> div_by_1
   1.203 +    nonzero_mult_divide_cancel_left ~> nonzero_mult_div_cancel_left
   1.204 +    div_mult_self1_is_id ~> nonzero_mult_div_cancel_left
   1.205 +    nonzero_mult_divide_cancel_right ~> nonzero_mult_div_cancel_right
   1.206 +    div_mult_self2_is_id ~> nonzero_mult_div_cancel_right
   1.207 +    is_unit_divide_mult_cancel_left ~> is_unit_div_mult_cancel_left
   1.208 +    is_unit_divide_mult_cancel_right ~> is_unit_div_mult_cancel_right
   1.209 +    mod_div_equality ~> div_mult_mod_eq
   1.210 +    mod_div_equality2 ~> mult_div_mod_eq
   1.211 +    mod_div_equality3 ~> mod_div_mult_eq
   1.212 +    mod_div_equality4 ~> mod_mult_div_eq
   1.213 +    minus_div_eq_mod ~> minus_div_mult_eq_mod
   1.214 +    minus_div_eq_mod2 ~> minus_mult_div_eq_mod
   1.215 +    minus_mod_eq_div ~> minus_mod_eq_div_mult
   1.216 +    minus_mod_eq_div2 ~> minus_mod_eq_mult_div
   1.217 +    div_mod_equality' ~> minus_mod_eq_div_mult [symmetric]
   1.218 +    mod_div_equality' ~> minus_div_mult_eq_mod [symmetric]
   1.219 +    zmod_zdiv_equality ~> mult_div_mod_eq [symmetric]
   1.220 +    zmod_zdiv_equality' ~> minus_div_mult_eq_mod [symmetric]
   1.221 +    Divides.mult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
   1.222 +    mult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
   1.223 +    zmult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
   1.224 +    div_1 ~> div_by_Suc_0
   1.225 +    mod_1 ~> mod_by_Suc_0
   1.226 +INCOMPATIBILITY.
   1.227 +
   1.228 +* New type class "idom_abs_sgn" specifies algebraic properties
   1.229 +of sign and absolute value functions.  Type class "sgn_if" has
   1.230 +disappeared.  Slight INCOMPATIBILITY.
   1.231 +
   1.232 +* Dedicated syntax LENGTH('a) for length of types.
   1.233 +
   1.234  * Characters (type char) are modelled as finite algebraic type
   1.235  corresponding to {0..255}.
   1.236  
   1.237 @@ -406,14 +413,11 @@
   1.238  
   1.239  * Static evaluators (Code_Evaluation.static_* in Isabelle/ML) rely on
   1.240  explicitly provided auxiliary definitions for required type class
   1.241 -dictionaries rather than half-working magic.  INCOMPATIBILITY, see
   1.242 -the tutorial on code generation for details.
   1.243 -
   1.244 -* Theory Set_Interval.thy: substantial new theorems on indexed sums
   1.245 -and products.
   1.246 -
   1.247 -* Theory List.thy: ranaming of listsum ~> sum_list, listprod ~>
   1.248 -prod_list, INCOMPATIBILITY.
   1.249 +dictionaries rather than half-working magic. INCOMPATIBILITY, see the
   1.250 +tutorial on code generation for details.
   1.251 +
   1.252 +* Theory Set_Interval: substantial new theorems on indexed sums and
   1.253 +products.
   1.254  
   1.255  * Locale bijection establishes convenient default simp rules such as
   1.256  "inv f (f a) = a" for total bijections.
   1.257 @@ -466,354 +470,6 @@
   1.258  
   1.259  * Added class topological_monoid.
   1.260  
   1.261 -* HOL-Library: theory FinFun bundles "finfun_syntax" and
   1.262 -"no_finfun_syntax" allow to control optional syntax in local contexts;
   1.263 -this supersedes former theory FinFun_Syntax. INCOMPATIBILITY, e.g. use
   1.264 -"unbundle finfun_syntax" to imitate import of
   1.265 -"~~/src/HOL/Library/FinFun_Syntax".
   1.266 -
   1.267 -* HOL-Library: theory Multiset_Permutations (executably) defines the set of
   1.268 -permutations of a given set or multiset, i.e. the set of all lists that
   1.269 -contain every element of the carrier (multi-)set exactly once.
   1.270 -
   1.271 -* HOL-Library: multiset membership is now expressed using set_mset
   1.272 -rather than count.
   1.273 -
   1.274 -  - Expressions "count M a > 0" and similar simplify to membership
   1.275 -    by default.
   1.276 -
   1.277 -  - Converting between "count M a = 0" and non-membership happens using
   1.278 -    equations count_eq_zero_iff and not_in_iff.
   1.279 -
   1.280 -  - Rules count_inI and in_countE obtain facts of the form
   1.281 -    "count M a = n" from membership.
   1.282 -
   1.283 -  - Rules count_in_diffI and in_diff_countE obtain facts of the form
   1.284 -    "count M a = n + count N a" from membership on difference sets.
   1.285 -
   1.286 -INCOMPATIBILITY.
   1.287 -
   1.288 -* HOL-Library: theory LaTeXsugar uses new-style "dummy_pats" for
   1.289 -displaying equations in functional programming style --- variables
   1.290 -present on the left-hand but not on the righ-hand side are replaced by
   1.291 -underscores.
   1.292 -
   1.293 -* HOL-Library: theory Combinator_PER provides combinator to build
   1.294 -partial equivalence relations from a predicate and an equivalence
   1.295 -relation.
   1.296 -
   1.297 -* HOL-Library: theory Perm provides basic facts about almost everywhere
   1.298 -fix bijections.
   1.299 -
   1.300 -* HOL-Library: theory Normalized_Fraction allows viewing an element of a
   1.301 -field of fractions as a normalized fraction (i.e. a pair of numerator
   1.302 -and denominator such that the two are coprime and the denominator is
   1.303 -normalized wrt. unit factors).
   1.304 -
   1.305 -* Session HOL-NSA has been renamed to HOL-Nonstandard_Analysis.
   1.306 -
   1.307 -* Session HOL-Multivariate_Analysis has been renamed to HOL-Analysis.
   1.308 -
   1.309 -* HOL-Analysis: measure theory has been moved here from HOL-Probability.
   1.310 -When importing HOL-Analysis some theorems need additional name spaces
   1.311 -prefixes due to name clashes. INCOMPATIBILITY.
   1.312 -
   1.313 -* HOL-Analysis: more complex analysis including Cauchy's inequality,
   1.314 -Liouville theorem, open mapping theorem, maximum modulus principle,
   1.315 -Residue theorem, Schwarz Lemma.
   1.316 -
   1.317 -* HOL-Analysis: Theory of polyhedra: faces, extreme points, polytopes,
   1.318 -and the Krein–Milman Minkowski theorem.
   1.319 -
   1.320 -* HOL-Analysis: Numerous results ported from the HOL Light libraries:
   1.321 -homeomorphisms, continuous function extensions, invariance of domain.
   1.322 -
   1.323 -* HOL-Probability: the type of emeasure and nn_integral was changed from
   1.324 -ereal to ennreal, INCOMPATIBILITY.
   1.325 -
   1.326 -  emeasure :: 'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal
   1.327 -  nn_integral :: 'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ennreal
   1.328 -
   1.329 -* HOL-Probability: Code generation and QuickCheck for Probability Mass
   1.330 -Functions.
   1.331 -
   1.332 -* HOL-Probability: theory Random_Permutations contains some theory about
   1.333 -choosing a permutation of a set uniformly at random and folding over a
   1.334 -list in random order.
   1.335 -
   1.336 -* HOL-Probability: theory SPMF formalises discrete subprobability
   1.337 -distributions.
   1.338 -
   1.339 -* HOL-Number_Theory: algebraic foundation for primes: Generalisation of
   1.340 -predicate "prime" and introduction of predicates "prime_elem",
   1.341 -"irreducible", a "prime_factorization" function, and the
   1.342 -"factorial_ring" typeclass with instance proofs for nat, int, poly. Some
   1.343 -theorems now have different names, most notably "prime_def" is now
   1.344 -"prime_nat_iff". INCOMPATIBILITY.
   1.345 -
   1.346 -* HOL-Library: the names of multiset theorems have been normalised to
   1.347 -distinguish which ordering the theorems are about
   1.348 -
   1.349 -    mset_less_eqI ~> mset_subset_eqI
   1.350 -    mset_less_insertD ~> mset_subset_insertD
   1.351 -    mset_less_eq_count ~> mset_subset_eq_count
   1.352 -    mset_less_diff_self ~> mset_subset_diff_self
   1.353 -    mset_le_exists_conv ~> mset_subset_eq_exists_conv
   1.354 -    mset_le_mono_add_right_cancel ~> mset_subset_eq_mono_add_right_cancel
   1.355 -    mset_le_mono_add_left_cancel ~> mset_subset_eq_mono_add_left_cancel
   1.356 -    mset_le_mono_add ~> mset_subset_eq_mono_add
   1.357 -    mset_le_add_left ~> mset_subset_eq_add_left
   1.358 -    mset_le_add_right ~> mset_subset_eq_add_right
   1.359 -    mset_le_single ~> mset_subset_eq_single
   1.360 -    mset_le_multiset_union_diff_commute ~> mset_subset_eq_multiset_union_diff_commute
   1.361 -    diff_le_self ~> diff_subset_eq_self
   1.362 -    mset_leD ~> mset_subset_eqD
   1.363 -    mset_lessD ~> mset_subsetD
   1.364 -    mset_le_insertD ~> mset_subset_eq_insertD
   1.365 -    mset_less_of_empty ~> mset_subset_of_empty
   1.366 -    mset_less_size ~> mset_subset_size
   1.367 -    wf_less_mset_rel ~> wf_subset_mset_rel
   1.368 -    count_le_replicate_mset_le ~> count_le_replicate_mset_subset_eq
   1.369 -    mset_remdups_le ~> mset_remdups_subset_eq
   1.370 -    ms_lesseq_impl ~> subset_eq_mset_impl
   1.371 -
   1.372 -Some functions have been renamed:
   1.373 -    ms_lesseq_impl -> subset_eq_mset_impl
   1.374 -
   1.375 -* HOL-Library: multisets are now ordered with the multiset ordering
   1.376 -    #\<subseteq># ~> \<le>
   1.377 -    #\<subset># ~> <
   1.378 -    le_multiset ~> less_eq_multiset
   1.379 -    less_multiset ~> le_multiset
   1.380 -INCOMPATIBILITY.
   1.381 -
   1.382 -* HOL-Library: the prefix multiset_order has been discontinued: the
   1.383 -theorems can be directly accessed. As a consequence, the lemmas
   1.384 -"order_multiset" and "linorder_multiset" have been discontinued, and the
   1.385 -interpretations "multiset_linorder" and "multiset_wellorder" have been
   1.386 -replaced by instantiations. INCOMPATIBILITY.
   1.387 -
   1.388 -* HOL-Library: some theorems about the multiset ordering have been
   1.389 -renamed:
   1.390 -
   1.391 -    le_multiset_def ~> less_eq_multiset_def
   1.392 -    less_multiset_def ~> le_multiset_def
   1.393 -    less_eq_imp_le_multiset ~> subset_eq_imp_le_multiset
   1.394 -    mult_less_not_refl ~> mset_le_not_refl
   1.395 -    mult_less_trans ~> mset_le_trans
   1.396 -    mult_less_not_sym ~> mset_le_not_sym
   1.397 -    mult_less_asym ~> mset_le_asym
   1.398 -    mult_less_irrefl ~> mset_le_irrefl
   1.399 -    union_less_mono2{,1,2} ~> union_le_mono2{,1,2}
   1.400 -
   1.401 -    le_multiset\<^sub>H\<^sub>O ~> less_eq_multiset\<^sub>H\<^sub>O
   1.402 -    le_multiset_total ~> less_eq_multiset_total
   1.403 -    less_multiset_right_total ~> subset_eq_imp_le_multiset
   1.404 -    le_multiset_empty_left ~> less_eq_multiset_empty_left
   1.405 -    le_multiset_empty_right ~> less_eq_multiset_empty_right
   1.406 -    less_multiset_empty_right ~> le_multiset_empty_left
   1.407 -    less_multiset_empty_left ~> le_multiset_empty_right
   1.408 -    union_less_diff_plus ~> union_le_diff_plus
   1.409 -    ex_gt_count_imp_less_multiset ~> ex_gt_count_imp_le_multiset
   1.410 -    less_multiset_plus_left_nonempty ~> le_multiset_plus_left_nonempty
   1.411 -    le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty
   1.412 -INCOMPATIBILITY.
   1.413 -
   1.414 -* HOL-Library: the lemma mset_map has now the attribute [simp].
   1.415 -INCOMPATIBILITY.
   1.416 -
   1.417 -* HOL-Library: some theorems about multisets have been removed.
   1.418 -INCOMPATIBILITY, use the following replacements:
   1.419 -
   1.420 -    le_multiset_plus_plus_left_iff ~> add_less_cancel_right
   1.421 -    less_multiset_plus_plus_left_iff ~> add_less_cancel_right
   1.422 -    le_multiset_plus_plus_right_iff ~> add_less_cancel_left
   1.423 -    less_multiset_plus_plus_right_iff ~> add_less_cancel_left
   1.424 -    add_eq_self_empty_iff ~> add_cancel_left_right
   1.425 -    mset_subset_add_bothsides ~> subset_mset.add_less_cancel_right
   1.426 -    mset_less_add_bothsides ~> subset_mset.add_less_cancel_right
   1.427 -    mset_le_add_bothsides ~> subset_mset.add_less_cancel_right
   1.428 -    empty_inter ~> subset_mset.inf_bot_left
   1.429 -    inter_empty ~> subset_mset.inf_bot_right
   1.430 -    empty_sup ~> subset_mset.sup_bot_left
   1.431 -    sup_empty ~> subset_mset.sup_bot_right
   1.432 -    bdd_below_multiset ~> subset_mset.bdd_above_bot
   1.433 -    subset_eq_empty ~> subset_mset.le_zero_eq
   1.434 -    le_empty ~> subset_mset.le_zero_eq
   1.435 -    mset_subset_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero
   1.436 -    mset_less_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero
   1.437 -
   1.438 -* HOL-Library: some typeclass constraints about multisets have been
   1.439 -reduced from ordered or linordered to preorder. Multisets have the
   1.440 -additional typeclasses order_bot, no_top,
   1.441 -ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add,
   1.442 -linordered_cancel_ab_semigroup_add, and
   1.443 -ordered_ab_semigroup_monoid_add_imp_le. INCOMPATIBILITY.
   1.444 -
   1.445 -* HOL-Library: there are some new simplification rules about multisets,
   1.446 -the multiset ordering, and the subset ordering on multisets.
   1.447 -INCOMPATIBILITY.
   1.448 -
   1.449 -* HOL-Library: the subset ordering on multisets has now the
   1.450 -interpretations ordered_ab_semigroup_monoid_add_imp_le and
   1.451 -bounded_lattice_bot. INCOMPATIBILITY.
   1.452 -
   1.453 -* HOL-Library/Multiset: single has been removed in favor of add_mset
   1.454 -that roughly corresponds to Set.insert. Some theorems have removed or
   1.455 -changed:
   1.456 -
   1.457 -  single_not_empty ~> add_mset_not_empty or empty_not_add_mset
   1.458 -  fold_mset_insert ~> fold_mset_add_mset
   1.459 -  image_mset_insert ~> image_mset_add_mset
   1.460 -  union_single_eq_diff
   1.461 -  multi_self_add_other_not_self
   1.462 -  diff_single_eq_union
   1.463 -INCOMPATIBILITY.
   1.464 -
   1.465 -* HOL-Library/Multiset: some theorems have been changed to use add_mset
   1.466 -instead of single:
   1.467 -
   1.468 -  mset_add
   1.469 -  multi_self_add_other_not_self
   1.470 -  diff_single_eq_union
   1.471 -  union_single_eq_diff
   1.472 -  union_single_eq_member
   1.473 -  add_eq_conv_diff
   1.474 -  insert_noteq_member
   1.475 -  add_eq_conv_ex
   1.476 -  multi_member_split
   1.477 -  multiset_add_sub_el_shuffle
   1.478 -  mset_subset_eq_insertD
   1.479 -  mset_subset_insertD
   1.480 -  insert_subset_eq_iff
   1.481 -  insert_union_subset_iff
   1.482 -  multi_psub_of_add_self
   1.483 -  inter_add_left1
   1.484 -  inter_add_left2
   1.485 -  inter_add_right1
   1.486 -  inter_add_right2
   1.487 -  sup_union_left1
   1.488 -  sup_union_left2
   1.489 -  sup_union_right1
   1.490 -  sup_union_right2
   1.491 -  size_eq_Suc_imp_eq_union
   1.492 -  multi_nonempty_split
   1.493 -  mset_insort
   1.494 -  mset_update
   1.495 -  mult1I
   1.496 -  less_add
   1.497 -  mset_zip_take_Cons_drop_twice
   1.498 -  rel_mset_Zero
   1.499 -  msed_map_invL
   1.500 -  msed_map_invR
   1.501 -  msed_rel_invL
   1.502 -  msed_rel_invR
   1.503 -  le_multiset_right_total
   1.504 -  multiset_induct
   1.505 -  multiset_induct2_size
   1.506 -  multiset_induct2
   1.507 -INCOMPATIBILITY.
   1.508 -
   1.509 -* HOL-Library/Multiset. The definitions of some constants have changed
   1.510 -to use add_mset instead of adding a single element:
   1.511 -  image_mset
   1.512 -  mset
   1.513 -  replicate_mset
   1.514 -  mult1
   1.515 -  pred_mset
   1.516 -  rel_mset'
   1.517 -  mset_insort
   1.518 -INCOMPATIBILITY.
   1.519 -
   1.520 -* HOL-Library/Multiset. Due to the above changes, the attributes of some
   1.521 -multiset theorems have been changed:
   1.522 -  insert_DiffM  [] ~> [simp]
   1.523 -  insert_DiffM2 [simp] ~> []
   1.524 -  diff_add_mset_swap [simp]
   1.525 -  fold_mset_add_mset [simp]
   1.526 -  diff_diff_add [simp] (for multisets only)
   1.527 -  diff_cancel [simp] ~> []
   1.528 -  count_single [simp] ~> []
   1.529 -  set_mset_single [simp] ~> []
   1.530 -  size_multiset_single [simp] ~> []
   1.531 -  size_single [simp] ~> []
   1.532 -  image_mset_single [simp] ~> []
   1.533 -  mset_subset_eq_mono_add_right_cancel [simp] ~> []
   1.534 -  mset_subset_eq_mono_add_left_cancel [simp] ~> []
   1.535 -  fold_mset_single [simp] ~> []
   1.536 -  subset_eq_empty [simp] ~> []
   1.537 -  empty_sup [simp] ~> []
   1.538 -  sup_empty [simp] ~> []
   1.539 -  inter_empty [simp] ~> []
   1.540 -  empty_inter [simp] ~> []
   1.541 -INCOMPATIBILITY.
   1.542 -
   1.543 -* HOL-Library/Multiset. The order of the variables in the second cases
   1.544 -of multiset_induct, multiset_induct2_size, multiset_induct2 has been
   1.545 -changed (e.g. Add A a ~> Add a A). INCOMPATIBILITY.
   1.546 -
   1.547 -* HOL-Library/Multiset. There is now a simplification procedure on
   1.548 -multisets. It mimics the behavior of the procedure on natural numbers.
   1.549 -INCOMPATIBILITY.
   1.550 -
   1.551 -* HOL-Library/Multiset. Renamed sums and products of multisets:
   1.552 -  msetsum ~> sum_mset
   1.553 -  msetprod ~> prod_mset
   1.554 -
   1.555 -* HOL-Library/Multiset. The notation for intersection and union of
   1.556 -multisets have been changed:
   1.557 -  #\<inter> ~> \<inter>#
   1.558 -  #\<union> ~> \<union>#
   1.559 -INCOMPATIBILITY.
   1.560 -
   1.561 -* HOL-Library/Multiset. The lemma one_step_implies_mult_aux on multisets
   1.562 -has been removed, use one_step_implies_mult instead. INCOMPATIBILITY.
   1.563 -
   1.564 -* The following theorems have been renamed:
   1.565 -  setsum_left_distrib ~> setsum_distrib_right
   1.566 -  setsum_right_distrib ~> setsum_distrib_left
   1.567 -INCOMPATIBILITY.
   1.568 -
   1.569 -* Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
   1.570 -INCOMPATIBILITY.
   1.571 -
   1.572 -* "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional
   1.573 -comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f ` A)".
   1.574 -
   1.575 -* Class semiring_Lcd merged into semiring_Gcd.  INCOMPATIBILITY.
   1.576 -
   1.577 -* The type class ordered_comm_monoid_add is now called
   1.578 -ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add
   1.579 -is introduced as the combination of ordered_ab_semigroup_add +
   1.580 -comm_monoid_add. INCOMPATIBILITY.
   1.581 -
   1.582 -* Introduced the type classes canonically_ordered_comm_monoid_add and
   1.583 -dioid.
   1.584 -
   1.585 -* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When
   1.586 -instantiating linordered_semiring_strict and ordered_ab_group_add, an
   1.587 -explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might
   1.588 -be required. INCOMPATIBILITY.
   1.589 -
   1.590 -* HOL-Library: theory Complete_Partial_Order2 provides reasoning support
   1.591 -for monotonicity and continuity in chain-complete partial orders and
   1.592 -about admissibility conditions for fixpoint inductions.
   1.593 -
   1.594 -* HOL-Library: theory Polynomial contains also derivation of polynomials
   1.595 -but not gcd/lcm on polynomials over fields. This has been moved to a
   1.596 -separate theory Library/Polynomial_GCD_euclidean.thy, to pave way for a
   1.597 -possible future different type class instantiation for polynomials over
   1.598 -factorial rings. INCOMPATIBILITY.
   1.599 -
   1.600 -* HOL-Library: theory Sublist.thy provides function "prefixes" with the
   1.601 -following renaming
   1.602 -
   1.603 -  prefixeq -> prefix
   1.604 -  prefix -> strict_prefix
   1.605 -  suffixeq -> suffix
   1.606 -  suffix -> strict_suffix
   1.607 -
   1.608 -Added theory of longest common prefixes.
   1.609  
   1.610  * Dropped various legacy fact bindings, whose replacements are often
   1.611  of a more general type also:
   1.612 @@ -910,15 +566,376 @@
   1.613  * Renamed HOL/Quotient_Examples/FSet.thy to
   1.614  HOL/Quotient_Examples/Quotient_FSet.thy INCOMPATIBILITY.
   1.615  
   1.616 -* The "nunchaku" program integrates the Nunchaku model finder. The tool
   1.617 -is experimental. See ~~/src/HOL/Nunchaku/Nunchaku.thy for details.
   1.618 +* Session HOL-Library: theory FinFun bundles "finfun_syntax" and
   1.619 +"no_finfun_syntax" allow to control optional syntax in local contexts;
   1.620 +this supersedes former theory FinFun_Syntax. INCOMPATIBILITY, e.g. use
   1.621 +"unbundle finfun_syntax" to imitate import of
   1.622 +"~~/src/HOL/Library/FinFun_Syntax".
   1.623 +
   1.624 +* Session HOL-Library: theory Multiset_Permutations (executably) defines
   1.625 +the set of permutations of a given set or multiset, i.e. the set of all
   1.626 +lists that contain every element of the carrier (multi-)set exactly
   1.627 +once.
   1.628 +
   1.629 +* Session HOL-Library: multiset membership is now expressed using
   1.630 +set_mset rather than count.
   1.631 +
   1.632 +  - Expressions "count M a > 0" and similar simplify to membership
   1.633 +    by default.
   1.634 +
   1.635 +  - Converting between "count M a = 0" and non-membership happens using
   1.636 +    equations count_eq_zero_iff and not_in_iff.
   1.637 +
   1.638 +  - Rules count_inI and in_countE obtain facts of the form
   1.639 +    "count M a = n" from membership.
   1.640 +
   1.641 +  - Rules count_in_diffI and in_diff_countE obtain facts of the form
   1.642 +    "count M a = n + count N a" from membership on difference sets.
   1.643 +
   1.644 +INCOMPATIBILITY.
   1.645 +
   1.646 +* Session HOL-Library: theory LaTeXsugar uses new-style "dummy_pats" for
   1.647 +displaying equations in functional programming style --- variables
   1.648 +present on the left-hand but not on the righ-hand side are replaced by
   1.649 +underscores.
   1.650 +
   1.651 +* Session HOL-Library: theory Combinator_PER provides combinator to
   1.652 +build partial equivalence relations from a predicate and an equivalence
   1.653 +relation.
   1.654 +
   1.655 +* Session HOL-Library: theory Perm provides basic facts about almost
   1.656 +everywhere fix bijections.
   1.657 +
   1.658 +* Session HOL-Library: theory Normalized_Fraction allows viewing an
   1.659 +element of a field of fractions as a normalized fraction (i.e. a pair of
   1.660 +numerator and denominator such that the two are coprime and the
   1.661 +denominator is normalized wrt. unit factors).
   1.662 +
   1.663 +* Session HOL-NSA has been renamed to HOL-Nonstandard_Analysis.
   1.664 +
   1.665 +* Session HOL-Multivariate_Analysis has been renamed to HOL-Analysis.
   1.666 +
   1.667 +* Session HOL-Analysis: measure theory has been moved here from
   1.668 +HOL-Probability. When importing HOL-Analysis some theorems need
   1.669 +additional name spaces prefixes due to name clashes. INCOMPATIBILITY.
   1.670 +
   1.671 +* Session HOL-Analysis: more complex analysis including Cauchy's
   1.672 +inequality, Liouville theorem, open mapping theorem, maximum modulus
   1.673 +principle, Residue theorem, Schwarz Lemma.
   1.674 +
   1.675 +* Session HOL-Analysis: Theory of polyhedra: faces, extreme points,
   1.676 +polytopes, and the Krein–Milman Minkowski theorem.
   1.677 +
   1.678 +* Session HOL-Analysis: Numerous results ported from the HOL Light
   1.679 +libraries: homeomorphisms, continuous function extensions, invariance of
   1.680 +domain.
   1.681 +
   1.682 +* Session HOL-Probability: the type of emeasure and nn_integral was
   1.683 +changed from ereal to ennreal, INCOMPATIBILITY.
   1.684 +
   1.685 +  emeasure :: 'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal
   1.686 +  nn_integral :: 'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ennreal
   1.687 +
   1.688 +* Session HOL-Probability: Code generation and QuickCheck for
   1.689 +Probability Mass Functions.
   1.690 +
   1.691 +* Session HOL-Probability: theory Random_Permutations contains some
   1.692 +theory about choosing a permutation of a set uniformly at random and
   1.693 +folding over a list in random order.
   1.694 +
   1.695 +* Session HOL-Probability: theory SPMF formalises discrete
   1.696 +subprobability distributions.
   1.697 +
   1.698 +* Session HOL-Number_Theory: algebraic foundation for primes:
   1.699 +Generalisation of predicate "prime" and introduction of predicates
   1.700 +"prime_elem", "irreducible", a "prime_factorization" function, and the
   1.701 +"factorial_ring" typeclass with instance proofs for nat, int, poly. Some
   1.702 +theorems now have different names, most notably "prime_def" is now
   1.703 +"prime_nat_iff". INCOMPATIBILITY.
   1.704 +
   1.705 +* Session Old_Number_Theory has been removed, after porting remaining
   1.706 +theories.
   1.707 +
   1.708 +* Session HOL-Library: the names of multiset theorems have been
   1.709 +normalised to distinguish which ordering the theorems are about
   1.710 +
   1.711 +    mset_less_eqI ~> mset_subset_eqI
   1.712 +    mset_less_insertD ~> mset_subset_insertD
   1.713 +    mset_less_eq_count ~> mset_subset_eq_count
   1.714 +    mset_less_diff_self ~> mset_subset_diff_self
   1.715 +    mset_le_exists_conv ~> mset_subset_eq_exists_conv
   1.716 +    mset_le_mono_add_right_cancel ~> mset_subset_eq_mono_add_right_cancel
   1.717 +    mset_le_mono_add_left_cancel ~> mset_subset_eq_mono_add_left_cancel
   1.718 +    mset_le_mono_add ~> mset_subset_eq_mono_add
   1.719 +    mset_le_add_left ~> mset_subset_eq_add_left
   1.720 +    mset_le_add_right ~> mset_subset_eq_add_right
   1.721 +    mset_le_single ~> mset_subset_eq_single
   1.722 +    mset_le_multiset_union_diff_commute ~> mset_subset_eq_multiset_union_diff_commute
   1.723 +    diff_le_self ~> diff_subset_eq_self
   1.724 +    mset_leD ~> mset_subset_eqD
   1.725 +    mset_lessD ~> mset_subsetD
   1.726 +    mset_le_insertD ~> mset_subset_eq_insertD
   1.727 +    mset_less_of_empty ~> mset_subset_of_empty
   1.728 +    mset_less_size ~> mset_subset_size
   1.729 +    wf_less_mset_rel ~> wf_subset_mset_rel
   1.730 +    count_le_replicate_mset_le ~> count_le_replicate_mset_subset_eq
   1.731 +    mset_remdups_le ~> mset_remdups_subset_eq
   1.732 +    ms_lesseq_impl ~> subset_eq_mset_impl
   1.733 +
   1.734 +Some functions have been renamed:
   1.735 +    ms_lesseq_impl -> subset_eq_mset_impl
   1.736 +
   1.737 +* The following theorems have been renamed:
   1.738 +
   1.739 +  setsum_left_distrib ~> setsum_distrib_right
   1.740 +  setsum_right_distrib ~> setsum_distrib_left
   1.741 +
   1.742 +INCOMPATIBILITY.
   1.743 +
   1.744 +* Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
   1.745 +INCOMPATIBILITY.
   1.746 +
   1.747 +* "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional
   1.748 +comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f `
   1.749 +A)".
   1.750 +
   1.751 +* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY.
   1.752 +
   1.753 +* The type class ordered_comm_monoid_add is now called
   1.754 +ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add
   1.755 +is introduced as the combination of ordered_ab_semigroup_add +
   1.756 +comm_monoid_add. INCOMPATIBILITY.
   1.757 +
   1.758 +* Introduced the type classes canonically_ordered_comm_monoid_add and
   1.759 +dioid.
   1.760 +
   1.761 +* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When
   1.762 +instantiating linordered_semiring_strict and ordered_ab_group_add, an
   1.763 +explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might
   1.764 +be required. INCOMPATIBILITY.
   1.765 +
   1.766 +* HOL-Library: multisets are now ordered with the multiset ordering
   1.767 +    #\<subseteq># ~> \<le>
   1.768 +    #\<subset># ~> <
   1.769 +    le_multiset ~> less_eq_multiset
   1.770 +    less_multiset ~> le_multiset
   1.771 +INCOMPATIBILITY.
   1.772 +
   1.773 +* Session HOL-Library: the prefix multiset_order has been discontinued:
   1.774 +the theorems can be directly accessed. As a consequence, the lemmas
   1.775 +"order_multiset" and "linorder_multiset" have been discontinued, and the
   1.776 +interpretations "multiset_linorder" and "multiset_wellorder" have been
   1.777 +replaced by instantiations. INCOMPATIBILITY.
   1.778 +
   1.779 +* Session HOL-Library: some theorems about the multiset ordering have
   1.780 +been renamed:
   1.781 +
   1.782 +    le_multiset_def ~> less_eq_multiset_def
   1.783 +    less_multiset_def ~> le_multiset_def
   1.784 +    less_eq_imp_le_multiset ~> subset_eq_imp_le_multiset
   1.785 +    mult_less_not_refl ~> mset_le_not_refl
   1.786 +    mult_less_trans ~> mset_le_trans
   1.787 +    mult_less_not_sym ~> mset_le_not_sym
   1.788 +    mult_less_asym ~> mset_le_asym
   1.789 +    mult_less_irrefl ~> mset_le_irrefl
   1.790 +    union_less_mono2{,1,2} ~> union_le_mono2{,1,2}
   1.791 +
   1.792 +    le_multiset\<^sub>H\<^sub>O ~> less_eq_multiset\<^sub>H\<^sub>O
   1.793 +    le_multiset_total ~> less_eq_multiset_total
   1.794 +    less_multiset_right_total ~> subset_eq_imp_le_multiset
   1.795 +    le_multiset_empty_left ~> less_eq_multiset_empty_left
   1.796 +    le_multiset_empty_right ~> less_eq_multiset_empty_right
   1.797 +    less_multiset_empty_right ~> le_multiset_empty_left
   1.798 +    less_multiset_empty_left ~> le_multiset_empty_right
   1.799 +    union_less_diff_plus ~> union_le_diff_plus
   1.800 +    ex_gt_count_imp_less_multiset ~> ex_gt_count_imp_le_multiset
   1.801 +    less_multiset_plus_left_nonempty ~> le_multiset_plus_left_nonempty
   1.802 +    le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty
   1.803 +INCOMPATIBILITY.
   1.804 +
   1.805 +* Session HOL-Library: the lemma mset_map has now the attribute [simp].
   1.806 +INCOMPATIBILITY.
   1.807 +
   1.808 +* Session HOL-Library: some theorems about multisets have been removed.
   1.809 +INCOMPATIBILITY, use the following replacements:
   1.810 +
   1.811 +    le_multiset_plus_plus_left_iff ~> add_less_cancel_right
   1.812 +    less_multiset_plus_plus_left_iff ~> add_less_cancel_right
   1.813 +    le_multiset_plus_plus_right_iff ~> add_less_cancel_left
   1.814 +    less_multiset_plus_plus_right_iff ~> add_less_cancel_left
   1.815 +    add_eq_self_empty_iff ~> add_cancel_left_right
   1.816 +    mset_subset_add_bothsides ~> subset_mset.add_less_cancel_right
   1.817 +    mset_less_add_bothsides ~> subset_mset.add_less_cancel_right
   1.818 +    mset_le_add_bothsides ~> subset_mset.add_less_cancel_right
   1.819 +    empty_inter ~> subset_mset.inf_bot_left
   1.820 +    inter_empty ~> subset_mset.inf_bot_right
   1.821 +    empty_sup ~> subset_mset.sup_bot_left
   1.822 +    sup_empty ~> subset_mset.sup_bot_right
   1.823 +    bdd_below_multiset ~> subset_mset.bdd_above_bot
   1.824 +    subset_eq_empty ~> subset_mset.le_zero_eq
   1.825 +    le_empty ~> subset_mset.le_zero_eq
   1.826 +    mset_subset_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero
   1.827 +    mset_less_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero
   1.828 +
   1.829 +* Session HOL-Library: some typeclass constraints about multisets have
   1.830 +been reduced from ordered or linordered to preorder. Multisets have the
   1.831 +additional typeclasses order_bot, no_top,
   1.832 +ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add,
   1.833 +linordered_cancel_ab_semigroup_add, and
   1.834 +ordered_ab_semigroup_monoid_add_imp_le. INCOMPATIBILITY.
   1.835 +
   1.836 +* Session HOL-Library: there are some new simplification rules about
   1.837 +multisets, the multiset ordering, and the subset ordering on multisets.
   1.838 +INCOMPATIBILITY.
   1.839 +
   1.840 +* Session HOL-Library: the subset ordering on multisets has now the
   1.841 +interpretations ordered_ab_semigroup_monoid_add_imp_le and
   1.842 +bounded_lattice_bot. INCOMPATIBILITY.
   1.843 +
   1.844 +* Session HOL-Library, theory Multiset: single has been removed in favor
   1.845 +of add_mset that roughly corresponds to Set.insert. Some theorems have
   1.846 +removed or changed:
   1.847 +
   1.848 +  single_not_empty ~> add_mset_not_empty or empty_not_add_mset
   1.849 +  fold_mset_insert ~> fold_mset_add_mset
   1.850 +  image_mset_insert ~> image_mset_add_mset
   1.851 +  union_single_eq_diff
   1.852 +  multi_self_add_other_not_self
   1.853 +  diff_single_eq_union
   1.854 +INCOMPATIBILITY.
   1.855 +
   1.856 +* Session HOL-Library, theory Multiset: some theorems have been changed
   1.857 +to use add_mset instead of single:
   1.858 +
   1.859 +  mset_add
   1.860 +  multi_self_add_other_not_self
   1.861 +  diff_single_eq_union
   1.862 +  union_single_eq_diff
   1.863 +  union_single_eq_member
   1.864 +  add_eq_conv_diff
   1.865 +  insert_noteq_member
   1.866 +  add_eq_conv_ex
   1.867 +  multi_member_split
   1.868 +  multiset_add_sub_el_shuffle
   1.869 +  mset_subset_eq_insertD
   1.870 +  mset_subset_insertD
   1.871 +  insert_subset_eq_iff
   1.872 +  insert_union_subset_iff
   1.873 +  multi_psub_of_add_self
   1.874 +  inter_add_left1
   1.875 +  inter_add_left2
   1.876 +  inter_add_right1
   1.877 +  inter_add_right2
   1.878 +  sup_union_left1
   1.879 +  sup_union_left2
   1.880 +  sup_union_right1
   1.881 +  sup_union_right2
   1.882 +  size_eq_Suc_imp_eq_union
   1.883 +  multi_nonempty_split
   1.884 +  mset_insort
   1.885 +  mset_update
   1.886 +  mult1I
   1.887 +  less_add
   1.888 +  mset_zip_take_Cons_drop_twice
   1.889 +  rel_mset_Zero
   1.890 +  msed_map_invL
   1.891 +  msed_map_invR
   1.892 +  msed_rel_invL
   1.893 +  msed_rel_invR
   1.894 +  le_multiset_right_total
   1.895 +  multiset_induct
   1.896 +  multiset_induct2_size
   1.897 +  multiset_induct2
   1.898 +INCOMPATIBILITY.
   1.899 +
   1.900 +* Session HOL-Library, theory Multiset: the definitions of some
   1.901 +constants have changed to use add_mset instead of adding a single
   1.902 +element:
   1.903 +
   1.904 +  image_mset
   1.905 +  mset
   1.906 +  replicate_mset
   1.907 +  mult1
   1.908 +  pred_mset
   1.909 +  rel_mset'
   1.910 +  mset_insort
   1.911 +
   1.912 +INCOMPATIBILITY.
   1.913 +
   1.914 +* Session HOL-Library, theory Multiset: due to the above changes, the
   1.915 +attributes of some multiset theorems have been changed:
   1.916 +
   1.917 +  insert_DiffM  [] ~> [simp]
   1.918 +  insert_DiffM2 [simp] ~> []
   1.919 +  diff_add_mset_swap [simp]
   1.920 +  fold_mset_add_mset [simp]
   1.921 +  diff_diff_add [simp] (for multisets only)
   1.922 +  diff_cancel [simp] ~> []
   1.923 +  count_single [simp] ~> []
   1.924 +  set_mset_single [simp] ~> []
   1.925 +  size_multiset_single [simp] ~> []
   1.926 +  size_single [simp] ~> []
   1.927 +  image_mset_single [simp] ~> []
   1.928 +  mset_subset_eq_mono_add_right_cancel [simp] ~> []
   1.929 +  mset_subset_eq_mono_add_left_cancel [simp] ~> []
   1.930 +  fold_mset_single [simp] ~> []
   1.931 +  subset_eq_empty [simp] ~> []
   1.932 +  empty_sup [simp] ~> []
   1.933 +  sup_empty [simp] ~> []
   1.934 +  inter_empty [simp] ~> []
   1.935 +  empty_inter [simp] ~> []
   1.936 +INCOMPATIBILITY.
   1.937 +
   1.938 +* Session HOL-Library, theory Multiset: The order of the variables in
   1.939 +the second cases of multiset_induct, multiset_induct2_size,
   1.940 +multiset_induct2 has been changed (e.g. Add A a ~> Add a A).
   1.941 +INCOMPATIBILITY.
   1.942 +
   1.943 +* Session HOL-Library, theory Multiset: there is now a simplification
   1.944 +procedure on multisets. It mimics the behavior of the procedure on
   1.945 +natural numbers. INCOMPATIBILITY.
   1.946 +
   1.947 +* Session HOL-Library, theory Multiset: renamed sums and products of
   1.948 +multisets:
   1.949 +
   1.950 +  msetsum ~> sum_mset
   1.951 +  msetprod ~> prod_mset
   1.952 +
   1.953 +* Session HOL-Library, theory Multiset: the notation for intersection
   1.954 +and union of multisets have been changed:
   1.955 +
   1.956 +  #\<inter> ~> \<inter>#
   1.957 +  #\<union> ~> \<union>#
   1.958 +
   1.959 +INCOMPATIBILITY.
   1.960 +
   1.961 +* Session HOL-Library, theory Multiset: the lemma
   1.962 +one_step_implies_mult_aux on multisets has been removed, use
   1.963 +one_step_implies_mult instead. INCOMPATIBILITY.
   1.964 +
   1.965 +* Session HOL-Library: theory Complete_Partial_Order2 provides reasoning
   1.966 +support for monotonicity and continuity in chain-complete partial orders
   1.967 +and about admissibility conditions for fixpoint inductions.
   1.968 +
   1.969 +* Session HOL-Library: theory Polynomial contains also derivation of
   1.970 +polynomials but not gcd/lcm on polynomials over fields. This has been
   1.971 +moved to a separate theory Library/Polynomial_GCD_euclidean.thy, to pave
   1.972 +way for a possible future different type class instantiation for
   1.973 +polynomials over factorial rings. INCOMPATIBILITY.
   1.974 +
   1.975 +* Session HOL-Library: theory Sublist provides function "prefixes" with
   1.976 +the following renaming
   1.977 +
   1.978 +  prefixeq -> prefix
   1.979 +  prefix -> strict_prefix
   1.980 +  suffixeq -> suffix
   1.981 +  suffix -> strict_suffix
   1.982 +
   1.983 +Added theory of longest common prefixes.
   1.984  
   1.985  
   1.986  *** ML ***
   1.987  
   1.988 -* ML antiquotation @{path} is superseded by @{file}, which ensures that
   1.989 -the argument is a plain file. Minor INCOMPATIBILITY.
   1.990 -
   1.991  * Integer.gcd and Integer.lcm use efficient operations from the Poly/ML
   1.992  library (notably for big integers). Subtle change of semantics:
   1.993  Integer.gcd and Integer.lcm both normalize the sign, results are never
   1.994 @@ -933,16 +950,19 @@
   1.995  use + instead of +/ etc. Moreover, exception Rat.DIVZERO has been
   1.996  superseded by General.Div.
   1.997  
   1.998 +* ML antiquotation @{path} is superseded by @{file}, which ensures that
   1.999 +the argument is a plain file. Minor INCOMPATIBILITY.
  1.1000 +
  1.1001 +* Antiquotation @{make_string} is available during Pure bootstrap --
  1.1002 +with approximative output quality.
  1.1003 +
  1.1004 +* Low-level ML system structures (like PolyML and RunCall) are no longer
  1.1005 +exposed to Isabelle/ML user-space. Potential INCOMPATIBILITY.
  1.1006 +
  1.1007  * The ML function "ML" provides easy access to run-time compilation.
  1.1008  This is particularly useful for conditional compilation, without
  1.1009  requiring separate files.
  1.1010  
  1.1011 -* Low-level ML system structures (like PolyML and RunCall) are no longer
  1.1012 -exposed to Isabelle/ML user-space. Potential INCOMPATIBILITY.
  1.1013 -
  1.1014 -* Antiquotation @{make_string} is available during Pure bootstrap --
  1.1015 -with approximative output quality.
  1.1016 -
  1.1017  * Option ML_exception_debugger controls detailed exception trace via the
  1.1018  Poly/ML debugger. Relevant ML modules need to be compiled beforehand
  1.1019  with ML_file_debug, or with ML_file and option ML_debugger enabled. Note
  1.1020 @@ -972,31 +992,10 @@
  1.1021  
  1.1022  *** System ***
  1.1023  
  1.1024 -* Isabelle/Scala: the SSH module supports ssh and sftp connections, for
  1.1025 -remote command-execution and file-system access. This resembles
  1.1026 -operations from module File and Isabelle_System to some extent. Note
  1.1027 -that Path specifications need to be resolved remotely via
  1.1028 -ssh.remote_path instead of File.standard_path: the implicit process
  1.1029 -environment is different, Isabelle settings are not available remotely.
  1.1030 -
  1.1031 -* Isabelle/Scala: the Mercurial module supports repositories via the
  1.1032 -regular hg command-line interface. The repositroy clone and working
  1.1033 -directory may reside on a local or remote file-system (via ssh
  1.1034 -connection).
  1.1035 -
  1.1036 -* Many Isabelle tools that require a Java runtime system refer to the
  1.1037 -settings ISABELLE_TOOL_JAVA_OPTIONS32 / ISABELLE_TOOL_JAVA_OPTIONS64,
  1.1038 -depending on the underlying platform. The settings for "isabelle build"
  1.1039 -ISABELLE_BUILD_JAVA_OPTIONS32 / ISABELLE_BUILD_JAVA_OPTIONS64 have been
  1.1040 -discontinued. Potential INCOMPATIBILITY.
  1.1041 -
  1.1042 -* The Isabelle system environment always ensures that the main
  1.1043 -executables are found within the shell search $PATH: "isabelle" and
  1.1044 -"isabelle_scala_script".
  1.1045 -
  1.1046 -* Isabelle tools may consist of .scala files: the Scala compiler is
  1.1047 -invoked on the spot. The source needs to define some object that extends
  1.1048 -Isabelle_Tool.Body.
  1.1049 +* SML/NJ and old versions of Poly/ML are no longer supported.
  1.1050 +
  1.1051 +* Poly/ML heaps now follow the hierarchy of sessions, and thus require
  1.1052 +much less disk space.
  1.1053  
  1.1054  * The Isabelle ML process is now managed directly by Isabelle/Scala, and
  1.1055  shell scripts merely provide optional command-line access. In
  1.1056 @@ -1016,30 +1015,14 @@
  1.1057  given heap image. Errors lead to premature exit of the ML process with
  1.1058  return code 1.
  1.1059  
  1.1060 -* The system option "threads" (for the size of the Isabelle/ML thread
  1.1061 -farm) is also passed to the underlying ML runtime system as --gcthreads,
  1.1062 +* The command-line tool "isabelle build" supports option -N for cyclic
  1.1063 +shuffling of NUMA CPU nodes. This may help performance tuning on Linux
  1.1064 +servers with separate CPU/memory modules.
  1.1065 +
  1.1066 +* System option "threads" (for the size of the Isabelle/ML thread farm)
  1.1067 +is also passed to the underlying ML runtime system as --gcthreads,
  1.1068  unless there is already a default provided via ML_OPTIONS settings.
  1.1069  
  1.1070 -* Command-line tool "isabelle console" provides option -r to help to
  1.1071 -bootstrapping Isabelle/Pure interactively.
  1.1072 -
  1.1073 -* Command-line tool "isabelle yxml" has been discontinued.
  1.1074 -INCOMPATIBILITY, use operations from the modules "XML" and "YXML" in
  1.1075 -Isabelle/ML or Isabelle/Scala.
  1.1076 -
  1.1077 -* File.bash_string, File.bash_path etc. represent Isabelle/ML and
  1.1078 -Isabelle/Scala strings authentically within GNU bash. This is useful to
  1.1079 -produce robust shell scripts under program control, without worrying
  1.1080 -about spaces or special characters. Note that user output works via
  1.1081 -Path.print (ML) or Path.toString (Scala). INCOMPATIBILITY, the old (and
  1.1082 -less versatile) operations File.shell_quote, File.shell_path etc. have
  1.1083 -been discontinued.
  1.1084 -
  1.1085 -* SML/NJ and old versions of Poly/ML are no longer supported.
  1.1086 -
  1.1087 -* Poly/ML heaps now follow the hierarchy of sessions, and thus require
  1.1088 -much less disk space.
  1.1089 -
  1.1090  * System option "checkpoint" helps to fine-tune the global heap space
  1.1091  management of isabelle build. This is relevant for big sessions that may
  1.1092  exhaust the small 32-bit address space of the ML process (which is used
  1.1093 @@ -1055,13 +1038,50 @@
  1.1094  multiprocessor systems. The "isabelle jedit" tool allows to override the
  1.1095  implicit default via option -p.
  1.1096  
  1.1097 +* Command-line tool "isabelle console" provides option -r to help to
  1.1098 +bootstrapping Isabelle/Pure interactively.
  1.1099 +
  1.1100 +* Command-line tool "isabelle yxml" has been discontinued.
  1.1101 +INCOMPATIBILITY, use operations from the modules "XML" and "YXML" in
  1.1102 +Isabelle/ML or Isabelle/Scala.
  1.1103 +
  1.1104 +* Many Isabelle tools that require a Java runtime system refer to the
  1.1105 +settings ISABELLE_TOOL_JAVA_OPTIONS32 / ISABELLE_TOOL_JAVA_OPTIONS64,
  1.1106 +depending on the underlying platform. The settings for "isabelle build"
  1.1107 +ISABELLE_BUILD_JAVA_OPTIONS32 / ISABELLE_BUILD_JAVA_OPTIONS64 have been
  1.1108 +discontinued. Potential INCOMPATIBILITY.
  1.1109 +
  1.1110 +* The Isabelle system environment always ensures that the main
  1.1111 +executables are found within the shell search $PATH: "isabelle" and
  1.1112 +"isabelle_scala_script".
  1.1113 +
  1.1114 +* Isabelle tools may consist of .scala files: the Scala compiler is
  1.1115 +invoked on the spot. The source needs to define some object that extends
  1.1116 +Isabelle_Tool.Body.
  1.1117 +
  1.1118 +* File.bash_string, File.bash_path etc. represent Isabelle/ML and
  1.1119 +Isabelle/Scala strings authentically within GNU bash. This is useful to
  1.1120 +produce robust shell scripts under program control, without worrying
  1.1121 +about spaces or special characters. Note that user output works via
  1.1122 +Path.print (ML) or Path.toString (Scala). INCOMPATIBILITY, the old (and
  1.1123 +less versatile) operations File.shell_quote, File.shell_path etc. have
  1.1124 +been discontinued.
  1.1125 +
  1.1126  * The isabelle_java executable allows to run a Java process within the
  1.1127  name space of Java and Scala components that are bundled with Isabelle,
  1.1128  but without the Isabelle settings environment.
  1.1129  
  1.1130 -* The command-line tool "isabelle build" supports option -N for cyclic
  1.1131 -shuffling of NUMA CPU nodes. This may help performance tuning on Linux
  1.1132 -servers with separate CPU/memory modules.
  1.1133 +* Isabelle/Scala: the SSH module supports ssh and sftp connections, for
  1.1134 +remote command-execution and file-system access. This resembles
  1.1135 +operations from module File and Isabelle_System to some extent. Note
  1.1136 +that Path specifications need to be resolved remotely via
  1.1137 +ssh.remote_path instead of File.standard_path: the implicit process
  1.1138 +environment is different, Isabelle settings are not available remotely.
  1.1139 +
  1.1140 +* Isabelle/Scala: the Mercurial module supports repositories via the
  1.1141 +regular hg command-line interface. The repositroy clone and working
  1.1142 +directory may reside on a local or remote file-system (via ssh
  1.1143 +connection).
  1.1144  
  1.1145  
  1.1146