Laurent Fousse writes: According to the google code page, it's actually BSD. The text in the LICENSE file [1] actually differs from the BSD license. It requires that changes are clearly documented and it does not require that redistribution in binary form reproduces the copyright. I am going to ask the upstream author whether he intended a BSD license. Bye, Hendrik [1] http://code.google.com/p/hol-light/source/browse/trunk/LICENSE