[isabelle-dev] Factorials and binomial coefficients
ac638 at cam.ac.uk
Thu Jan 29 16:42:17 CET 2009
For now HOL/Fact.thy defines factorials (over natural numbers) and
strangely imports the reals. The theorem involving the reals, however,
hold in any (ordered) (ring/field) of charachteristic Zero.
Apart from that, I have a formalization of Pochhammer's symbol (raising
factorials) which generalize factorials (I have also relation theorems
to fact) and the generalized binomial coefficient.
Since Fact.thy is needed for building HOL but Library/Binomial is not,
my question is whether we should unify these two developments or should
I add my formalization into Libray or ex? Any comments are welcome!
More information about the isabelle-dev