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

[Makarius]

On Wed, 26 Jun 2013, Stephen Nuchia wrote:

> Finally, I make my living in the commercial software world and I do not 
> generally own the intellectual property I work on.  I will often be less 
> than completely open about the details of my work.  I regret that but 
> it's necessary.

Concerning anything that ends up in the Isabelle repository, it needs to 
conform to the "ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER" of its 
central COPYRIGHT file, with some potential add-on information in 
CONTRIBUTORS and/or in individual file headers (at most one line as part 
of "Author" info).

Intellectual property remains to whoever "owns" it, but by definition 
these "owners" agree on the one Isabelle license.  Thus you never need to 
decide about ownership in practice -- the license takes precedence for all 
relevant situations.  This is a nice consequence of classical logic in a 
real-world situation.

Interestingly, the Coq guys -- being constructivists -- try to make this 
decidable, by asking transfer of "IP ownership" of contributors, although 
that is very hard to implement.


 	Makarius