Re: [isabelle] Isabelle and latex questions

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 {*

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)

  TermStyle.add_style "no_all_prem1" (style_parm_premise 1) #>
  TermStyle.add_style "no_all_prem2" (style_parm_premise 2)

Now you can go @{thm_style no_all_prem1 my_induction_thm}

Warning: I have hardly tested this!


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

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