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


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?

Christian Doczkal

Attachment: smime.p7s
Description: S/MIME cryptographic signature

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