Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Mutually Recursive Partial Func...

Email Gateway (Aug 19 2022 at 13:36):

From: Tobias Nipkow <nipkow@in.tum.de>
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!

Email Gateway (Aug 19 2022 at 13:37):

From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
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.

Email Gateway (Aug 19 2022 at 13:37):

From: Tobias Nipkow <nipkow@in.tum.de>
Thanks, I have corrected it to BSD.

Tobias

Last updated: Apr 18 2024 at 01:05 UTC