Is there a realistic prospect for uniting these two formalisations of linear
> 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