Hi Amine,
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
Hi,
I left Fact.thy alone because it is necessary for building HOL. I moved
it upwards though (now it imports Nat instead of RealDef). I added the
other stuff to Binomial since it is Library stuff and not necessary
for building HOL.
This said, I have no objection (or strong opinion about) to
