*To*: Jesper Bengtson <jesperb at it.uu.se>*Subject*: Re: [isabelle] Isabelle and latex questions*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 14 Jul 2009 09:38:21 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <27CF0C57-2B85-4A39-A074-C53DC00E3230@it.uu.se>*References*: <27CF0C57-2B85-4A39-A074-C53DC00E3230@it.uu.se>*User-agent*: Thunderbird 2.0.0.22 (X11/20090605)

You can add your own styles for printing terms or theorems. Add the following to your theory. It declares your own styles "no_all_prem1" and "no_all_prem2" - you can add more if you like. setup {* let fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) = strip_assums_all ((a,T)::params, t) | strip_assums_all (params, B) = (params, B); fun style_parm_premise i ctxt t = let val prems = Logic.strip_imp_prems t in if i <= length prems then let val (params,t) = strip_assums_all([], nth prems (i - 1)) in subst_bounds(map Free params, t) end else error ("Not enough premises for prem" ^ string_of_int i ^ " in propositon: " ^ Syntax.string_of_term ctxt t) end; in TermStyle.add_style "no_all_prem1" (style_parm_premise 1) #> TermStyle.add_style "no_all_prem2" (style_parm_premise 2) end *} Now you can go @{thm_style no_all_prem1 my_induction_thm} Warning: I have hardly tested this! Tobias Jesper Bengtson wrote: > 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

**References**:**[isabelle] Isabelle and latex questions***From:*Jesper Bengtson

- Previous by Date: Re: [isabelle] set comprehension with pairs
- Next by Date: Re: [isabelle] set comprehension with pairs
- Previous by Thread: [isabelle] Isabelle and latex questions
- Next by Thread: Re: [isabelle] Isabelle and latex questions
- Cl-isabelle-users July 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list