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
