[isabelle-dev] Factorials and binomial coefficients

[Amine Chaieb]

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.