Dear all, 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! best wishes, Amine.
