[isabelle-dev] Future of Nat_Transfer

[Florian Haftmann]

See now http://isabelle.in.tum.de/repos/isabelle/rev/0230af0f3c59.

	Florian

Am 19.10.2017 um 13:56 schrieb 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
> 
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

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/20171104/cc81b266/attachment.asc>