[isabelle-dev] Future of Nat_Transfer

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20171019/fc3bc4bc/attachment.asc>