NEWS
changeset 73937 3708884bfa8a
parent 73928 7404f2e1d092
child 73938 78044b2f001c
equal deleted inserted replaced
73936:50437744eb1c 73937:3708884bfa8a
    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", "Perm" have been moved there from session
    86 "Multiset_Permutations", "Perm" have been moved there from session
    87 HOL-Library.  See theory "Guide" for an overview about existing material
    87 HOL-Library.
    88 on basic combinatorics.
       
    89 
    88 
    90 * Theory "Permutation" in HOL-Library has been renamed to the more
    89 * Theory "Permutation" in HOL-Library has been renamed to the more
    91 specific "List_Permutation".  Note that most notions from that
    90 specific "List_Permutation".  Note that most notions from that
    92 theory are already present in theory "Permutations".  INCOMPATIBILITY.
    91 theory are already present in theory "Permutations".  INCOMPATIBILITY.
    93 
    92