Summary
- move lemmas from new entry to proper theory; generalize ffact_Suc_rev
The file was modified | thys/Discrete_Summation/Factorials.thy (diff) |
The file was modified | thys/Discrete_Summation/Summation_Conversion.thy (diff) |
The file was modified | thys/Falling_Factorial_Sum/Falling_Factorial_Sum_Combinatorics.thy (diff) |
The file was modified | thys/Falling_Factorial_Sum/Falling_Factorial_Sum_Induction.thy (diff) |
The file was modified | thys/Falling_Factorial_Sum/Falling_Factorial_Sum_Vandermonde.thy (diff) |