Skip to content
Success

Changes

Summary

  1. simplified definitions of combinatorial functions
  2. define binomial coefficents directly via combinatorial definition
Changeset 63367:6c731c8b7f03 by haftmann:
simplified definitions of combinatorial functions
The file was modified src/HOL/Binomial.thy (diff)
The file was modified src/HOL/Library/Formal_Power_Series.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Gamma.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy (diff)
The file was modified src/HOL/NthRoot.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)
The file was modified src/HOL/ex/Sum_of_Powers.thy (diff)
Changeset 63366:209c4cbbc4cd by haftmann:
define binomial coefficents directly via combinatorial definition
The file was modified src/HOL/Binomial.thy (diff)