Skip to content
Failed

Changes

Summary

  1. move lemmas from new entry to proper theory; generalize ffact_Suc_rev
Changeset 8784:14c525483c56 by lukas bulwahn _lukas.bulwahn@gmail.com_:
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)