[isabelle-dev] Factorials and binomial coefficients

Lawrence Paulson lp15 at cam.ac.uk
Thu Jan 29 17:37:46 CET 2009

This ancient development deserves whatever reorganisation you feel is  

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

More information about the isabelle-dev mailing list