[isabelle] Isabelle and latex questions



Greetings all.

I am currently trying to typeset my thesis with the very nice latex generation capabilities that Isabelle provides. I have a few questions.

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?

Secondly, I have some very large induction rules which I would like to present and every case of these rules have all of their parameters meta-quantified. Is there a mode which removes the actual meta- quantification? It takes up a lot of space, and the absence of the quantifiers can be explained in figure captions in stead. What I would like to do is an equivalent of @{thm_style [mode=Rule] premxx myInductionRule}, but without the preceeding /\x y z ... . I'm guessing either a new style or mode is required.

I have been reading through the reference manual, but not found a way to do these things although I'm sure at least the second one is possible.

Many thanks.

/Jesper





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