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
--
Home:
http://wwwbroy.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
URL:
<https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20090202/c0cde9b8/attachment.pgp>
