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

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,
--
Holger

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