Dear all,

the nowadays ancient theory Nat_Transfer (essentially providing an
attribute to transfer ad-hoc between theorems on nat vs. int) is almost
obsolete:

* Ā»almostĀ« since I haven't figured out how relevant it is still for
HOL-Number_Theory

* Conversion between nat and int is rarely needed since most common
lemmas are provided by type classes anyway nowadays.

See also
http://isabelle.in.tum.de/repos/isabelle/file/ee874941dfb8/src/HOL/Nat_Transfer.thy
for the current state of affairs.

My suggestion would be to remove it completely.

Any opinions on that?

Cheers,
        Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to