Re: [isabelle] Print Heading *before* theory (nice to have)



Hi Holger,

if you want to have more control over theory headers, you should redinfe isamarkupheader in root.tex in the document directory. For example:

\renewcommand{\isamarkupheader}[1]{#1}

Then, you can use the usual LaTeX commands in header directly, e.g.:

header {* \section{Fibonacci} *}

or

header {* \subsection{Auxiliary stuff} *}

Best,
Andreas

On 16/10/13 11:50, Holger Blasum wrote:
Thanks Andreas, Lars,

On 10-16, Andreas Lochbihler wrote:
you can use the header command before the theory starts:
header {* Fibonacci *}
theory Fib imports Main begin

Works fine! Could I also generate subheaders this way (not all
thy files are of equal importance ...)? (I have not found a command
subheader yet.) I did notice the advice to use
  \renewcommand{\isamarkupheader}[1]{\subsection{#1}}
but putting that latex commend as text_raw *into* a (e.g., the preceding)
theory appears not to work as theory contents are appear to be
parsed after the headers.

thanks,





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