Session Twelvefold_Way
View
theory dependencies
View
document
View
outline
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