Re: [isabelle] Library of Proofs



On Sun, 29 Jan 2012, Jens Doll wrote:

Hello Isabelle,

since I was having some problems with directly using the examples from the web site (mixture of ASCII and Unicode; the HTML page source is even worse for reformatting), I'd suggest to offer the proof library in the same manner as the Cobol Test Suite is presented to the users. It's two small *.jsp pages and afterwards it looks like this:


http://cococo.de/Context_IT_GmbH/index.jsp?content=directory&lib=products/Sources/COBOL/

** Just a question : **

Would I be allowed to set up a mirror here for the University of Hamburg?

I also don't quite understand the problem, nor the purpose of a "mirror".

In general the BSD-style license of Isabelle allows you to work with the given sources in many ways, and present the results other servers, or keep them for yourself on a private storage device, or move them to /dev/null. Other people have done that before, while making clear that it is their own project that happens to use Isabelle in one way or the other.


	Makarius





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