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 merging these developments. Best wishes, Amine. Florian Haftmann wrote: > 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 >> 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! > > I would encourage to go the way through: replace Binomial/Fact by your > development. > > In the examples you sent with your rewrite orientation problem there is > still a separate Fact.thy (which a few dozens of lines). I would > strongly suggest to integrate this into your Binomal.thy > > Thanks a lot, > Florian >
