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

[Lawrence Paulson]

Is there a realistic prospect for uniting these two formalisations of linear algebra?
Larry

> On 27 Feb 2018, at 11:05, Thiemann, Rene <Rene.Thiemann at uibk.ac.at> wrote:
> 
> But indeed, Fabian is completely right that lemmas for determinants, etc. are duplicates. Actually, the JNF-matrices “‘a mat” 
> have been developed from scratch (without HMA_Connect), by manually copying and adapting several proofs from the distribution.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180227/f2111e78/attachment-0002.html>