The attached theory contains notes and a sketeched agenda to promote further algebra and number theory in Isabelle/HOL, esp. concerning gcd, div and mod – according to my current understanding of the whole matter.
I am looking forward to comments, and maybe contributors.
Personally, I will not put much time into this the next weeks but will
come back to it as soon as appropriate.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
Agenda_Algebra.thy
Description: application/extension-thy
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
