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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
