Session Twelvefold_Way

Theories

• HOL-Combinatorics.Transposition
• HOL-Combinatorics.Permutations
• HOL-ex.Birthday_Paradox
• HOL-Combinatorics.Stirling
• Card_Partitions.Set_Partition
• HOL-Eisbach.Eisbach
  • File ‹parse_tools.ML›
  • File ‹method_closure.ML›
  • File ‹eisbach_rule_insts.ML›
  • File ‹match_method.ML›
• Card_Partitions.Injectivity_Solver
• Card_Partitions.Card_Partitions
• Bell_Numbers_Spivey.Bell_Numbers
• Card_Multisets.Card_Multisets
• Card_Number_Partitions.Additions_to_Main
• Card_Number_Partitions.Number_Partition
• Card_Number_Partitions.Card_Number_Partitions
• Preliminaries
• Twelvefold_Way_Core
• Equiv_Relations_on_Functions
• Twelvefold_Way_Entry1
• Twelvefold_Way_Entry2
• Twelvefold_Way_Entry4
• Twelvefold_Way_Entry5
• Twelvefold_Way_Entry6
• Twelvefold_Way_Entry7
• Twelvefold_Way_Entry8
• Twelvefold_Way_Entry9
• Twelvefold_Way_Entry3
• Twelvefold_Way_Entry10
• Twelvefold_Way_Entry11
• Twelvefold_Way_Entry12
• Card_Bijections
• Card_Bijections_Direct
• Twelvefold_Way