Hi Manuel, > I am glad to announce that as of261d42f0bfac, Old_Number_Theory is > finally history.
these are good news indeed. One remark on the diff: + src/HOL/Number_Theory/QuadraticReciprocity.thy + src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy 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 theories anyway. > 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! Cheers, Florian -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev