Is there a realistic prospect for uniting these two formalisations of linear algebra? Larry
> On 27 Feb 2018, at 11:05, Thiemann, Rene <rene.thiem...@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.
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
