Re: [isabelle] New AFP entry: Mutually Recursive Partial Functions



Thanks, I have corrected it to BSD.

Tobias

On 19/02/2014 17:33, Yannick Duchêne (Hibou57) wrote:
> Le Wed, 19 Feb 2014 09:57:24 +0100, Tobias Nipkow <nipkow at in.tum.de> a écrit:
> 
>> Mutually Recursive Partial Functions
>> René Thiemann
>>
>> We provide a wrapper around the partial-function command that supports mutual
>> recursion.
>>
>> http://afp.sourceforge.net/entries/Partial_Function_MR.shtml
>>
>> Enjoy!
> 
> Excuse my ignorance on a topic, I never cared before.
> 
> This entry is marked “License: BSD License” on the main page, and is marked
> “License: LGPL” on these pages:
> 
>   *
> http://afp.sourceforge.net/browser_info/current/AFP/Partial_Function_MR/Partial_Function_MR.html
> 
>   *
> http://afp.sourceforge.net/browser_info/current/AFP/Partial_Function_MR/Partial_Function_MR_Examples.html
> 
> 
> As far as I know (I may be wrong), BSD inside (L)GPL is OK, but not the other way.
> 
> Also by the way, another question I've never ask: in which way the license of a
> theory impacts what's proved after that theory? One may have the same question
> with program generation.
> 
> 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.