Session Falling_Factorial_Sum
View
theory dependencies
View
document
View
outline
Theories
HOL-Combinatorics.Stirling
Discrete_Summation.Factorials
HOL-Eisbach.Eisbach
File ‹parse_tools.ML›
File ‹method_closure.ML›
File ‹eisbach_rule_insts.ML›
File ‹match_method.ML›
Card_Partitions.Injectivity_Solver
Falling_Factorial_Sum_Combinatorics
Falling_Factorial_Sum_Induction
Falling_Factorial_Sum_Vandermonde