# HG changeset patch
# User wenzelm
# Date 1623069622 -7200
# Node ID aefa7d210725d6719e7cd841e299d8194bcd9402
# Parent  201200b549fc582379089b41478c606f39927045
more formal theory and session names;
tuned whitespace;

diff -r 201200b549fc -r aefa7d210725 NEWS
--- a/NEWS	Mon Jun 07 14:34:55 2021 +0200
+++ b/NEWS	Mon Jun 07 14:40:22 2021 +0200
@@ -105,14 +105,14 @@
 
 *** HOL ***
 
-* Theory Multiset: dedicated predicate "multiset" is gone, use
-explict expression instead.  Minor INCOMPATIBILITY.
-
-* Theory Multiset: consolidated abbreviations Mempty, Melem, not_Melem
-to empty_mset, member_mset, not_member_mset respectively.  Minor
-INCOMPATIBILITY.
-
-* Theory Multiset: consolidated operation and fact names:
+* Theory "HOL-Library.Multiset": dedicated predicate "multiset" is gone,
+use explict expression instead. Minor INCOMPATIBILITY.
+
+* Theory "HOL-Library.Multiset": consolidated abbreviations Mempty,
+Melem, not_Melem to empty_mset, member_mset, not_member_mset
+respectively. Minor INCOMPATIBILITY.
+
+* Theory "HOL-Library.Multiset": consolidated operation and fact names:
     inf_subset_mset ~> inter_mset
     sup_subset_mset ~> union_mset
     multiset_inter_def ~> inter_mset_def
@@ -120,52 +120,52 @@
     multiset_inter_count ~> count_inter_mset
     sup_subset_mset_count ~> count_union_mset
 
-* Theory Multiset: syntax precendence for membership operations has been
-adjusted to match the corresponding precendences on sets.  Rare
-INCOMPATIBILITY.
-
-* HOL-Analysis/HOL-Probability: indexed products of discrete
-distributions, negative binomial distribution, Hoeffding's inequality,
-Chernoff bounds, Cauchy–Schwarz inequality for nn_integral, and some
-more small lemmas. Some theorems that were stated awkwardly before were
-corrected. Minor INCOMPATIBILITY.
+* Theory "HOL-Library.Multiset": syntax precendence for membership
+operations has been adjusted to match the corresponding precendences on
+sets. Rare INCOMPATIBILITY.
+
+* Session "HOL-Analysis" and "HOL-Probability": indexed products of
+discrete distributions, negative binomial distribution, Hoeffding's
+inequality, Chernoff bounds, Cauchy–Schwarz inequality for nn_integral,
+and some more small lemmas. Some theorems that were stated awkwardly
+before were corrected. Minor INCOMPATIBILITY.
 
 * Theorems "antisym" and "eq_iff" in class "order" have been renamed to
 "order.antisym" and "order.eq_iff", to coexist locally with "antisym"
-and "eq_iff" from locale "ordering".  INCOMPATIBILITY: significant
+and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant
 potential for change can be avoided if interpretations of type class
 "order" are replaced or augmented by interpretations of locale
 "ordering".
 
-* Theorem "swap_def" now is always qualified as "Fun.swap_def".  Minor
+* Theorem "swap_def" now is always qualified as "Fun.swap_def". Minor
 INCOMPATIBILITY; note that for most applications less elementary lemmas
 exists.
 
-* Dedicated session HOL-Combinatorics.  INCOMPATIBILITY: theories
+* Theory "HOL-Library.Permutation" has been renamed to the more specific
+"HOL-Library.List_Permutation". Note that most notions from that theory
+are already present in theory "HOL-Combinatorics.Permutations".
+INCOMPATIBILITY.
+
+* Dedicated session "HOL-Combinatorics". INCOMPATIBILITY: theories
 "Permutations", "List_Permutation" (formerly "Permutation"), "Stirling",
 "Multiset_Permutations", "Perm" have been moved there from session
 HOL-Library.
 
-* Theory "Permutation" in HOL-Library has been renamed to the more
-specific "List_Permutation".  Note that most notions from that
-theory are already present in theory "Permutations".  INCOMPATIBILITY.
-
-* Lemma "permutes_induct" has been given stronger
-hypotheses and named premises.  INCOMPATIBILITY.
-
-* Theory "Transposition" in HOL-Combinatorics provides elementary
-swap operation "transpose".
-
-* Combinator "Fun.swap" resolved into a mere input abbreviation
-in separate theory "Transposition" in HOL-Combinatorics.
-INCOMPATIBILITY.
+* Theory "HOL-Combinatorics.Transposition" provides elementary swap
+operation "transpose".
+
+* Lemma "permutes_induct" has been given stronger hypotheses and named
+premises. INCOMPATIBILITY.
+
+* Combinator "Fun.swap" resolved into a mere input abbreviation in
+separate theory "Transposition" in HOL-Combinatorics. INCOMPATIBILITY.
 
 * Bit operations set_bit, unset_bit and flip_bit are now class
-operations.  INCOMPATIBILITY.
+operations. INCOMPATIBILITY.
 
 * Abbreviation "max_word" has been moved to session Word_Lib in the AFP,
 as also have constants "shiftl1", "shiftr1", "sshiftr1", "bshiftr1",
-"setBit", "clearBit".  See there further the changelog in theory Guide.
+"setBit", "clearBit". See there further the changelog in theory Guide.
 INCOMPATIBILITY.