*To*: Peter Sewell <Peter.Sewell at cl.cam.ac.uk>*Subject*: Re: [isabelle] quoting definitions in latex*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 14 Dec 2007 17:08:56 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <E1J38zt-0004OF-00@mta2.cl.cam.ac.uk>*References*: <E1J38zt-0004OF-00@mta2.cl.cam.ac.uk>*User-agent*: Thunderbird 1.5.0.7 (X11/20060909)

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

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?

**Follow-Ups**:**Re: [isabelle] quoting definitions in latex***From:*Peter Sewell

**References**:**[isabelle] quoting definitions in latex***From:*Peter Sewell

- Previous by Date: [isabelle] quoting definitions in latex
- Next by Date: [isabelle] CFA: Transnational Access Programme at RISC
- Previous by Thread: [isabelle] quoting definitions in latex
- Next by Thread: Re: [isabelle] quoting definitions in latex
- Cl-isabelle-users December 2007 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