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-...@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

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