Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 19 2022 at 12:07):

From: Holger Blasum <hbl@sysgo.com>
Dear users,

if I encapsulate the fib function (from the tutorial) into
a file and want to give it a nice heading ("Fibonacci")
I recall I can use the "section" command.

$cat fib.thy
theory fib
imports Main
begin

section {* Fibonacci *}
fun fib :: "nat => nat" where
"fib 0 = 0" |
"fib (Suc 0) = 1" |
"fib (Suc(Suc x)) = fib x

+ fib (Suc x)

end

Then a generated PDF looks like this

theory fib
imports Main
begin
Fibonacci
fun fib :: nat => nat where
fib 0 = 0 |
fib (Suc 0 ) = 1 |
fib (Suc(Suc x )) = fib x

• fib (Suc x )
  end

Is there a simple and maintainable way to move
the content of the heading ("Fibonacci") before
"theory fib"?

thx,

Email Gateway (Aug 19 2022 at 12:07):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Holger,

you can use the header command before the theory starts:

header {* Fibonacci *}
theory Fib imports Main begin

Best,
Andreas

Email Gateway (Aug 19 2022 at 12:07):

From: Lars Noschinski <noschinl@in.tum.de>
You can use the "header" command.

-- Lars

Email Gateway (Aug 19 2022 at 12:07):

From: Holger Blasum <hbl@sysgo.com>
Thanks Andreas, Lars,

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,

Email Gateway (Aug 19 2022 at 12:07):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

Email Gateway (Aug 19 2022 at 12:07):

From: Holger Blasum <hbl@sysgo.com>
Hi Andreas,

Thanks, I hadn't realized root.tex was the proper location.
It now works!

Last updated: Apr 25 2024 at 16:19 UTC