[isabelle-dev] Factorials and binomial coefficients

[Lawrence Paulson]

This ancient development deserves whatever reorganisation you feel is  
appropriate.
Larry

On 29 Jan 2009, at 15:42, Amine Chaieb wrote:

> 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.
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev