Re: [isabelle] Library of Proofs



Am Sonntag, den 29.01.2012, 11:41 +0100 schrieb Jens Doll:
> 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/

Are you referring to the theory documentation like:
 
  https://isabelle.in.tum.de/dist/library/HOL/Complete_Lattices.html

You can copy the text from these pages and insert it into emacs and
jedit. jEdit has currently the problem to not transform the \<..> syntax
into unicode symbols, but you can work with it and it should be
correctly displayed if you reload the file.

Of course the generated HTML files should correctly display the unicode
symbols instead of the \<...> syntax. If you want to have a raw-file
accessd via HTTP you can also use the mercurial repository like:

   http://isabelle.in.tum.de/repos/isabelle/raw-file/Isabelle2011-1/src/HOL/Complete_Lattices.thy


> ** Just a question : **
> 
>  Would I be allowed to set up a mirror here for the University of Hamburg?

Why do you need the mirror?

I prefer to have as few mirrors as possible as they are often outdated,
have a different setup as the original page, and we can not mirror the
wiki pages.

Of course you need a mirror, you can copy the page with tools like wget
or you give us an rsync account and we duplicate our content.

> Jens








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