NEWS
changeset 73878 4dc3baf45d6a
parent 73872 b0ea03e837b1
child 73879 5020054b3a16
equal deleted inserted replaced
73877:b4b70d13c995 73878:4dc3baf45d6a
    81 INCOMPATIBILITY; note that for most applications less elementary lemmas
    81 INCOMPATIBILITY; note that for most applications less elementary lemmas
    82 exists.
    82 exists.
    83 
    83 
    84 * Dedicated session HOL-Combinatorics.  INCOMPATIBILITY: theories
    84 * Dedicated session HOL-Combinatorics.  INCOMPATIBILITY: theories
    85 "Permutations", "List_Permutation" (formerly "Permutation"), "Stirling",
    85 "Permutations", "List_Permutation" (formerly "Permutation"), "Stirling",
    86 "Multiset_Permutations"  have been
    86 "Multiset_Permutations", "Perm" have been moved there from session
    87 moved there from session HOL-Library.  See theory "Guide" for an
    87 HOL-Library.  See theory "Guide" for an overview about existing material
    88 overview about existing material on basic combinatorics.
    88 on basic combinatorics.
    89 
    89 
    90 * Theory "Permutation" in HOL-Library has been renamed to the more
    90 * Theory "Permutation" in HOL-Library has been renamed to the more
    91 specific "List_Permutation".  Note that most notions from that
    91 specific "List_Permutation".  Note that most notions from that
    92 theory are already present in theory "Permutations".  INCOMPATIBILITY.
    92 theory are already present in theory "Permutations".  INCOMPATIBILITY.
    93 
    93