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

Stephen Nuchia snuchia at gmail.com
Wed Jun 26 00:37:56 CEST 2013

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

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.


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>

More information about the isabelle-dev mailing list