Collecting arguments for licence change

[Achim D. Brucker]

Hi,
On Fri, May 28, 2004 at 11:14:48PM +0200, Frank Heckenbach wrote:
> 
> I know this answer is very late (I was quite busy recently). Just
> wanted to mention that your description reminded me a bit of GAP
> <http://www.gap-system.org>, a mathematical package for computation
> in discrete abstract algebra.
quite a good guess. The project I was talking about is Isabelle 
<http://isabelle.in.tum.de>, a generic, interactive theorem prover; or
in other wording: a mathematical package for computation in logic :-).
> 
> Previously GAP was released under a non-free license
> (non-commercial), but recently it changed to the GPL. The authors
> also are mostly of two European Universities. I don't know the
> details and discussions that led to the decision, but if (still)
> necessary, you could try to contact the responsible people ...
many thanks for your offer. Fortunately I can already report a success. 
After a intensive discussion about various licencing details the copyright 
holder of Isabelle decided to release future versions of Isabelle under 
the modified BSD license <http://www.opensource.org/licenses/bsd-license.php>.
Further, a new release of the latest Isabelle version (called "Isabelle 2004")
reflecting the licencing change will be provided).
Understandable, such a new release will take some time as most of the 
source files have to be modified. But the re-licencing was already
confirmed officially on the Isabelle mailing list (see message
<E1BV5u2-0005Ja-00 at mta1.cl.cam.ac.uk> in the mailing list archive:
http://www.cl.cam.ac.uk/users/lcp/archive/isabelle-users.04.gz ).

I'm very glad that Isabelle joins the group of free formal proof
tools. 

Achim