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

Le Wed, 19 Feb 2014 09:57:24 +0100, Tobias Nipkow <nipkow at> a écrit:

Mutually Recursive Partial Functions
René Thiemann

We provide a wrapper around the partial-function command that supports mutual


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:

* *

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.

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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