subject:"\[isabelle\-dev\] Future of Nat_Transfer"

Re: [isabelle-dev] Future of Nat_Transfer

2017-11-04 Thread 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 >

Re: [isabelle-dev] Future of Nat_Transfer

2017-10-19 Thread 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. > >