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



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,

-- 
Holger




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