[isabelle-dev] Factorials and binomial coefficients

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

[isabelle-dev] Factorials and binomial coefficients

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

[isabelle-dev] More Mercurial hints

A few more hints on using the Isabelle Mercurial repository smoothly, although most people should now this already. * The fetch extension takes care of most of the details of pull/update/merge, asking for user intervention only for non-trivial merges. hg fetch is configured by

[isabelle-dev] problems with the class-package

/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/13bea7a9