Re: [isabelle] Syntax issue: lost between HOL and Isar



On 8/1/2012 3:02 PM, Yannick Duchêne (Hibou57) wrote:

As the syntax from the PDF is not always exact (mainly characters issues)...

Yannick,

You can get the sources for any of the Isabelle2012 documentation.

The direct link is this:

http://isabelle.in.tum.de/repos/isabelle/archive/21c42b095c84.tar.gz

The link that would get you to the link for that file is here:

http://isabelle.in.tum.de/repos/isabelle/

You click on "files" beside "2 months ago Isabelle2012". You would then click on "gz" at the top of the page.

You unzip the tar file, and for isar-ref.pdf, you find the folder "isabelle-21c42b095c84\doc-src\IsarRef\Thy".

You then have to search around on those files with grep or something to find the file that contains the desired code.

The source files keep you from having to type in the code, keep you from copying bogus characters from the PDF, and they teach you something about how the author produced what you see in the PDF.

Regards,
GB








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