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

[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 :-)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130625/d4b44ac6/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: trace_mult_sym.hgbundle
Type: application/octet-stream
Size: 601 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130625/d4b44ac6/attachment.obj>