src/HOL/Binomial_Plus.thy
changeset 82407 fcc0f74ac086
parent 80654 10c712405854