[isabelle-dev] Smallest contribution ever (trace_mul_sym generalization)

[Tobias Nipkow]

It is best to communicate such changes to theories directly to the author of the
theory. Or enquire on isabelle-users who feels responsible for that theory to
get in touch with him. I guess your email is an instance of the "who feels
responsible" and Johannes will take care of it.

Thanks
Tobias

Am 26/06/2013 00:37, schrieb Stephen Nuchia:
> Just joined the list, still very much a beginner but I think the attached change
> is valid and desirable.  The theorem trace_mul_sym in
> HOL/Multivariate_Analysis/Determinants.thy is not stated in full generality;
> relaxing the restriction that the factor matrices be individually square is
> valid.  In fact, the original proof script succeeds unmodified.
> 
> I hope I am following proper "external contributor" protocol here.  I did not do
> the full battery of recommended pre-commitment tests because I haven't yet
> figured out how to switch my Cygwin environment to point at the local mercurial
> repository but I was able to build the relevant session in the HOL directory
> with the change replicated there.  I'm thinking I should spin up a VM or work
> under Linux for preparing changesets and keep my real work on the official
> release on my primary workstation.
> 
> -swn
> 
> The documentation for this change now outweighs the change itself by three
> orders of magnitude :-)
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>