Re: [isabelle] generating Isar code with screen font



Hi Gergely,

Is your ROOT file registered in any of the ROOTS files of the distribution? If not, you have to add the path to ROOT's folder to the search path using the option -d.

  isabelle build -d <path_to_ROOT_folder> -o browser_info -o document=pdf -v -c <session>

-o browser_info generates the HTML output similar to your example.
-o document=pdf generates the LaTeX documents, but they do not look like the HTML versions.

Hope this helps,
Andreas

On 05/07/16 15:27, Gergely Buday wrote:
I guess this is outside the document preparation system, but this is what I
would really want, in a pdf:

http://isabelle.in.tum.de/library/HOL/HOL/Code_Generator.html

I have found something in the System manual on page 22:

https://isabelle.in.tum.de/dist/Isabelle2016/doc/system.pdf#page=25

so I tried

    isabelle build -o browser_info -o document=pdf  -v -c isartutorial

for that I got

    *** Undefined session(s): "isartutorial"

where I used the session name in the ROOT file.

The examples in the System manual used library names, is this feature available only for them?

How can I define the session name for this?

- Gergely





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