Collecting arguments for licence change

Achim D. Brucker brucker at
Sun Jun 6 12:50:34 UTC 2004

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
> <>, a mathematical package for computation
> in discrete abstract algebra.
quite a good guess. The project I was talking about is Isabelle 
<>, 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 <>.
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> in the mailing list archive: ).

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


More information about the Discussion mailing list