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

> On 27 Feb 2018, at 11:05, Thiemann, Rene <> 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

Reply via email to