[isabelle-dev] Old_Number_Theory

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20161018/bab10d96/attachment.sig>