Re: [isabelle] Looking for the GOOD way to use Isabelle and Latex together when writing a thesis



On 15/05/12 03:21, Tobias Nipkow wrote:
> Maybe this helps: https://isabelle.in.tum.de/community/Generate_TeX_Snippets
> The example is a bit simple, but you can probably do something like this:
> 
> text_raw{*
> \DefineSnippet{name}{
> *}
> 
> <your Isabelle text>
> 
> text_raw{* } *}
> 
> However, I haven't tried this. I have another way of achieving what you want,
> but it needs a lengthier piece of latex code. I can send it to you if you want.

I used this sort of thing for my MSc thesis.  I used text (and sometimes
txt) instead of text_raw, and found it useful to include the %EndSnippet
comment suggested in the page Tobias linked to.  Together with the other
suggestions in that page, including using a Makefile, I found a solution
based on this that was adequate for my needs.

Tim
<><

Attachment: signature.asc
Description: OpenPGP digital signature



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