Re: [isabelle] quoting definitions in latex



You cannot quote type abbreviations but definitions work: @{thm f_def}

You may also want to look at "LaTeX sugar for proof documents" http://isabelle.in.tum.de/dist/Isabelle/doc/sugar.pdf

There is no way to display "!" etc as \forall, you need to write it that way in the first place - it's a subtle issue.

Tobias

Peter Sewell wrote:
Dear Isabelle,

I'd like to write an expository document based on some Isabelle, and
so need to quote selected definitions, not necessarily in the order
they appear in the main .thy.

I expect this is a standard and solved problem, but the Tutorial
doesn't seem to address it.  I can see how to quote (e.g.) type and
constant names, viz

  text {* @{typ event_structure} @{const writes} *}

but not the bodies of selected "types" or "constdefs" definitions...?

many thanks,
Peter


p.s.  While I'm here, could I appeal for _line numbers_ in the error
messages reported by the isabelle/proof-general combo?  I recall that
a couple of years ago we humble users (primarily Keith Wansbrough) had
to add line numbers to the HOL error messages, dragging that kicking
and screaming into the 1960s.  It'd be great if Isabelle could also catch up...:)

p.p.s.  Also, the LaTeX generated from my .thy by "isatool make"
doesn't typeset !, ?, --> etc with the proper LaTeX symbols.  Is there
any way to turn that on, without rewriting my sources with \<forall>
etc?








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