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 
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.



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