Re: [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-...@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

Re: [isabelle-dev] Future of Nat_Transfer

[Lawrence Paulson]

I have never understood it and generally feel terror at the sight of any 
transfer operation. So I would be happy to get rid of it.
Larry

> On 19 Oct 2017, at 12:56, Florian Haftmann 
>  wrote:
> 
> My suggestion would be to remove it completely.
> 
> Any opinions on that?

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