equal
deleted
inserted
replaced
1 (* Title: Binomial.thy |
1 (* Title: HOL/Number_Theory/Binomial.thy |
2 Authors: Lawrence C. Paulson, Jeremy Avigad, Tobias Nipkow |
2 Authors: Lawrence C. Paulson, Jeremy Avigad, Tobias Nipkow |
3 |
3 |
4 Defines the "choose" function, and establishes basic properties. |
4 Defines the "choose" function, and establishes basic properties. |
5 |
5 |
6 The original theory "Binomial" was by Lawrence C. Paulson, based on |
6 The original theory "Binomial" was by Lawrence C. Paulson, based on |