Re: [isabelle] generating Isar code with screen font



> 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.