Re: [isabelle] Isabelle and latex questions

On 10.07.2009, at 00:03, Jesper Bengtson wrote:

Firstly, when printing proofs, Isabelle does a very nice job of typesetting the keywords and indentations of the proof scripts, but the actual object logic terms keep their x-symbol syntax and not the nice latex sugar that I have defined for them. Is there any flag to set which would translate them in the same manner as is done when using the @{term...} antiquotation?

No there is not. You can only access the full power of syntax print translations through antiquotations.

Typically there are two kinds of documents typeset with Isabelle:
1) present the pure theory (or an Isabelle tutorial): mainly Isabelle proof text with documenting @{text } quotations and antiquotations. 2) write a document (like a thesis) about your theories: mainly a big @{text } quotation with heaps of antiquotations.



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