Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] "\include{}" for theory files?

Email Gateway (Aug 18 2022 at 13:03):

From: Christian Doczkal <c.doczkal@stud.uni-saarland.de>
Hello

I want to add some latex paragraphs to my (already lengthy) theory file
so I would like to write the latex code into a different file just like
one does with ordinary LaTeX. But Since all anti-quotations need to be
processed text {* \include{file} *} doesn't do the trick.

Is there some ML command that lets you "inline" other files to achieve
the desired effect?
smime.p7s

Email Gateway (Aug 18 2022 at 13:03):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christian,

why not split your theory into multiple ones?

Florian
signature.asc

Email Gateway (Aug 18 2022 at 13:03):

From: Makarius <makarius@sketis.net>
You can always use the 'text_raw' (or 'txt_raw') command to include
whatever LaTeX sources you need. So this should do the job:

text_raw {* \include{file} *}

Makarius

Last updated: May 03 2024 at 08:18 UTC