Re: [isabelle-dev] Fwd: [isabelle] Matrix-Vector operation

> Am 26.02.2018 um 16:12 schrieb Lawrence Paulson : > > I was at the meeting in Logroño and my impression was that we had to live > with these different formalisations. There was no way to unify them and the > best one could hope to transfer certain results from one

Re: [isabelle-dev] Fwd: [isabelle] Matrix-Vector operation

I was at the meeting in Logroño and my impression was that we had to live with these different formalisations. There was no way to unify them and the best one could hope to transfer certain results from one formalisation to another using local types in some incredibly complicated way. If there

Re: [isabelle-dev] Fwd: [isabelle] Matrix-Vector operation

> Am 26.02.2018 um 12:54 schrieb Lawrence Paulson : > > Is there a case for moving some material from this file into the Analysis > directory? > > https://www.isa-afp.org/browser_info/current/AFP/Perron_Frobenius/HMA_Connect.html > > Many of the results proved at the end of

[isabelle-dev] Fwd: [isabelle] Matrix-Vector operation

Is there a case for moving some material from this file into the Analysis directory? https://www.isa-afp.org/browser_info/current/AFP/Perron_Frobenius/HMA_Connect.html Many of the results proved at the end of