florian.haftmann at informatik.tu-muenchen.de
Tue Oct 18 13:30:38 CEST 2016
> I am glad to announce that as of261d42f0bfac, Old_Number_Theory is
> finally history.
these are good news indeed.
One remark on the diff:
This is a formal regression: a proper name has turned into CaMlCaSe.
But that should be easy to correct.
There is another pre-existing CaMlCaSe theory, MiscAlgebra; but from the
description of the theory itself this should go suitable HOL-Algebra
> A lot of the proofs are still quite messy and don't take advantage of
> the new features we now have in Number_Theory (such as a uniform concept
> of ‘primes’ and ‘prime factorisations’ for both nat and int), but I do
> not think the work necessary to achieve that is worth it.
Messy proofs can be amended in case of need. Messy definitions are more
critical since they may infect further theories, but all that seems to
have disappeared in the transition.
> The vast majority of the porting work was done by a student of ours,
> Jaime Mendizabal Roche, so big thanks to him. He even extended the ‘two
> squares’ AFP entry a bit, showing the converse direction as well.
Thanks a lot also!
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 819 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev