Hi Freek, On Fri, 12 Sep 2008, Freek Wiedijk wrote:
Mizar is thus the last major proof assistant whose sources are closed, and licensing unclear.I was in Japan recently, visiting Nobuki Takayama, and he told me that these licensing issues had been a reason for him not to put Mizar on his KNOPPIX/Math DVD (see <http://www.knoppix-math.org/>; it's a DVD with all kinds of mathematical software packages that you can boot from and then everything will just work.)
The same e.g. with David Wheeler's listing: http://www.dwheeler.com/essays/high-assurance-floss.html#theoremprovers . Non-FLOSS software is plainly ignored.
Josef