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